I'm messing about with a possible new core for Idris. I've got this far. It's surprising what you need to do to get this far...https://gist.github.com/edwinb/617c016e2380d46c12b6d0fda0891245 …
-
Show this thread
-
This rather ridiculous example typechecks about 30 times faster than Blodwen, so it's possible I should keep going on this one...https://gist.github.com/edwinb/56f6e9730b6a7ebca9f258f5222db6f4 …
3 replies 0 retweets 20 likesShow this thread -
Replying to @edwinbrady
This is huge! Does it impact Nat proofs (like type checking of LTE for a big natural and a small one)?
1 reply 0 retweets 1 like
Replying to @BeRewt
I don't know about what'll happen for realistic programs yet :). Haven't got as far as pattern matching.
12:27 AM - 7 Apr 2019
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.