rhi
0 Followers · 0 Following
  • Joined on 2020-06-10
Repositories
23
 Projects Packages Public Activity Starred Repositories
rhi pushed to 🐉 at rhi/quox 2023-11-10 09:07:32 -05:00
d115672d49 example stuff
rhi pushed to main at rhi/misc 2023-11-09 20:26:29 -05:00
e60a61ee76 add make-sizes
ae7e6c796d various tablet-setup tweaks
4adf34027f make nix develop less annoying
92a86afffe add ( ) to little
Compare 4 commits »
rhi pushed to 🐉 at rhi/quox 2023-11-06 16:11:14 -05:00
cc78ccd940 fix some parenthesisation
50984aa1aa refactor #[attribute] stuff
Compare 2 commits »
rhi pushed to 🐉 at rhi/quox 2023-11-05 10:10:40 -05:00
246d80eea2 add io.quox
c48b7be559 add html output highlighting
040a1862c3 refactor scheme prelude
bf8cced888 swap some delim/syntax highlighting around
04af7ae942 highlight the @ in dim apps as a delim
Compare 15 commits »
rhi pushed to main at rhi/idris2-vim 2023-11-05 06:10:51 -05:00
8d61704813 change highlight categories
8b12e7dd3e add %syntactic
Compare 2 commits »
rhi closed issue rhi/quox#32 2023-11-03 13:15:31 -04:00
add pair η to Whnf.Coercion
rhi commented on issue rhi/quox#32 2023-11-03 13:15:31 -04:00
add pair η to Whnf.Coercion

this is actually covered when a case gets rewritten to fst/snd in whnf

rhi deleted branch 🧼 from rhi/quox 2023-11-03 13:06:48 -04:00
rhi pushed to 🐉 at rhi/quox 2023-11-03 13:06:42 -04:00
d4639a35c6 add hello.quox to examples
b7e1f37b5b add some #[compile-scheme]
5dfefe443c more tidying of outputs
0514fff481 represent ℕ constants directly
fa7f82ae5a rename Nat to NAT in AST
Compare 33 commits »
rhi merged pull request rhi/quox#29 2023-11-03 13:06:42 -04:00
erasure and also baby's first scheme backend
rhi pushed to 🧼 at rhi/quox 2023-11-03 13:06:03 -04:00
d4639a35c6 add hello.quox to examples
b7e1f37b5b add some #[compile-scheme]
5dfefe443c more tidying of outputs
0514fff481 represent ℕ constants directly
fa7f82ae5a rename Nat to NAT in AST
Compare 32 commits »
rhi pushed to 🧼 at rhi/quox 2023-11-03 12:43:04 -04:00
310c20b73a add hello.quox to examples
f517517ce9 add some #[compile-scheme]
6d9e4656bf misc.All doesn't need to be a ★¹
baafa065c5 more tidying of outputs
58b2729ae0 represent ℕ constants directly
Compare 8 commits »
rhi opened issue rhi/quox#32 2023-11-02 13:04:07 -04:00
add pair η to Whnf.Coercion
rhi pushed to 🧼 at rhi/quox 2023-11-02 12:50:01 -04:00
55a6906c28 always vsep scheme lets, otherwise they are unreadable
ef6deade76 highlight errors even if real output is to a file
f40542441d add postulate, #[compile-scheme], #[main]
3bec2477d9 add pair.map-fst and pair.map-snd
Compare 4 commits »
rhi pushed to main at rhi/lang 2023-10-30 07:03:33 -04:00
669c4da1dc langfilter version bump
rhi pushed to main at rhi/lang 2023-10-30 04:47:04 -04:00
1136cff702 add <mark> syntax `*hello*`
abd27eebe9 allow-newer (fixme)
7ad0415e38 words
9d23f99948 add alt blockquote syntax to langfilter
Compare 4 commits »
rhi closed issue rhi/quox#31 2023-10-25 15:07:38 -04:00
pretty printing is SLOW
rhi commented on issue rhi/quox#31 2023-10-25 15:07:38 -04:00
pretty printing is SLOW

no it isn't, unless you put the entire output in a single document. oops

rhi opened issue rhi/quox#31 2023-10-21 14:46:07 -04:00
pretty printing is SLOW
rhi pushed to 🧼 at rhi/quox 2023-09-30 12:37:56 -04:00
c023845ed7 erasure to untyped syntax
8f8b282d07 add locations and substitutions to untyped syntax
9183111125 simplify isEmpty and isSubSing
99577c7ef2 add fail.quox to all.quox
2e8c71a369 tweak quantities in eta.from-false
Compare 6 commits »