rhi
0 Followers · 0 Following
  • Joined on 2020-06-10
Repositories
22
 Projects Packages Public Activity Starred Repositories
rhi pushed to 🌐 at rhi/yummy.cricket 2024-03-02 12:23:31 -05:00
749d22b8b8 id page and markup/css cleanup
45bc1a60b6 gradients
2d5b9aa618 fix for seamonkey
Compare 3 commits »
rhi pushed to 🐉 at rhi/quox 2024-02-28 10:49:33 -05:00
a8ac6f11f7 fix a quantity in CaseBox
rhi closed issue rhi/quox#38 2024-02-24 10:05:24 -05:00
type checker loop in pushCoe
rhi pushed to 🐉 at rhi/quox 2024-02-24 10:05:24 -05:00
b67162bda1 fix the other similar loops
24ae5b85a2 fix a broken test????
325e128063 add η for False and True
642ac25a71 happy new year [pack update. also idris 0.7.0]
05a688d49e reject "" in NatExtra.fromHex
Compare 12 commits »
rhi commented on issue rhi/quox#38 2024-02-13 19:45:24 -05:00
type checker loop in pushCoe

actually no the Π/Eq rules have the same problem after all lol

rhi reopened issue rhi/quox#38 2024-02-13 19:45:24 -05:00
type checker loop in pushCoe
rhi commented on pull request rhi/quox#39 2024-02-10 05:22:28 -05:00
WIP: log

quox -P check fin.quox

  • on 🐉 branch: 0.253 s
  • on this branch: 4.154 s

ughhhhh

rhi pushed to log at rhi/quox 2024-02-10 04:16:34 -05:00
8b8bec250a wip
103700d882 wip
642ac25a71 happy new year [pack update. also idris 0.7.0]
05a688d49e reject "" in NatExtra.fromHex
1c8c50f3e2 remove some unneeded Ord impls
Compare 12 commits »
rhi closed issue rhi/quox#38 2024-02-10 04:07:36 -05:00
type checker loop in pushCoe
rhi pushed to 🐉 at rhi/quox 2024-02-10 04:07:36 -05:00
81783dbae0 fix typechecker loop when coercing boxes
rhi commented on issue rhi/quox#38 2024-01-30 15:39:38 -05:00
type checker loop in pushCoe

i found it

it's the η expansion for boxes, in Q.Whnf.Coercion.pushCoe

in the function η expansions, you have something like

(coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
 …
rhi created pull request rhi/quox#39 2024-01-13 09:33:12 -05:00
WIP: log
rhi created branch log in rhi/quox 2024-01-13 09:32:21 -05:00
rhi pushed to log at rhi/quox 2024-01-13 09:32:21 -05:00
2de2bd1f04 wip
b804ceb8fe happy new year [pack update. also idris 0.7.0]
88355bf469 reject "" in NatExtra.fromHex
00716e9aba remove some unneeded Ord impls
ff04348683 remove most noLocs
Compare 10 commits »
rhi pushed to main at rhi/misc 2024-01-11 14:33:38 -05:00
38efa0ef7f make-sizes updates
rhi pushed to main at rhi/blog 2023-12-27 19:00:40 -05:00
32edbb1816 a bunch of stuff sorry
2910daf0c6 update deps
3aee53faa1 posts
Compare 3 commits »
rhi deleted branch new-glyphs from rhi/lang 2023-12-25 15:51:38 -05:00
rhi commented on pull request rhi/lang#1 2023-12-25 15:51:34 -05:00
WIP: new improved lántas script

i forgot i made a pr for this

rhi closed pull request rhi/lang#1 2023-12-25 15:51:34 -05:00
WIP: new improved lántas script
rhi pushed to main at rhi/lang 2023-12-25 15:51:12 -05:00
275490551b squash a warning
cb61556b17 words for xmas and halloween
a2dc61b428 lántas script updates
d44c407560 expand iksa (v)
14bcc959c9 fix a metadata typo
Compare 20 commits »