rhi
- Joined on Jun 10, 2020
Loading Heatmap…
-
629434c752 wip maybe.quox
-
e55ecaf5f6 some bitwise ops corresponding to OPE ops
-
3506b217b1 switch syntax to codb
-
e1e9ca1b80 split and extend Quox.Thin
-
b98b11b100 add Quox.Thin
- Compare 5 commits »
5 days ago
rhi pushed to main at rhi/idris2-vim
-
1cb34ab5d6 add type search on \s (since proof search is ALSO \o)
-
504979fe07 remove menu bar stuff
-
9c35464b69 also print input expression with \e
-
2c89714506 remove commands that don't exist in idris2
- Compare 4 commits »
2 weeks ago
rhi pushed to main at rhi/idris2-vim
-
518e5f0c41 fix refine command
-
ad08ee24f5 stop wobbling the window around on reload
- Compare 2 commits »
2 weeks ago
-
00e79d4264 quote names in Show
-
a11bedd62a update pack
-
c5fa11bdec don't need this agda file any more
- Compare 3 commits »
2 weeks ago
-
3bbf0366c8 make 0 in ★₀ optional
-
7c68cd9098 multimodal type theory bib
-
282565c7a3 Whnf ⇒ CanWhnf; WhnfM ⇒ Eff Whnf
-
2af8ee20ea those were not meant to stay there
-
42aa07c9c8 crude but effective stratification
- Compare 6 commits »
3 weeks ago
-
5930295380 make p,q in coe/comp optional and default to @0 @1
-
7b93a913c7 rewrite pretty printer
-
f6abf084b3 qty lub is total actually (usually ω)
-
ba755a9c4b haha oops
-
8d6ae6cc32 move location to the start of type errors
- Compare 5 commits »
4 weeks ago