The proto-Idris-2 doesn't have high level constructs yet, but it has Elaborator Reflection now so I'll probably implement the rest of it that way...https://gist.github.com/edwinb/18638589f9de62a6419c9c32e22a9edd …
-
-
Replying to @edwinbrady
What difference does it make to what ideis was doing? Would you mind explaining just a bit?
1 reply 0 retweets 0 likes
Replying to @PLT_cheater
The general idea is from https://eb.host.cs.st-andrews.ac.uk/drafts/elab-reflection.pdf … - I'm experimenting to see if the Self Hosting plan in §7.1 is remotely feasible
1:12 PM - 1 Apr 2018
0 replies
0 retweets
1 like
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.