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 …
-
-
Any inspiration taken from smalltt?
-
Yes, it preserves sharing of metavariables. Also I took the chance to represent global names more sensibly. It might get trickier when I add linearity checking, we'll see.
- 7 more replies
New conversation -
-
-
This is huge! Does it impact Nat proofs (like type checking of LTE for a big natural and a small one)?
-
I don't know about what'll happen for realistic programs yet :). Haven't got as far as pattern matching.
End of conversation
New conversation -
-
-
How long is this taking? Just tried this in Granule and it takes a ridiculous 4 seconds on my 2.3 GHz i5 (8 GB RAM).
-
I got 0.1s or so on my macbook. Profiling suggests there's a little more to be gained too... Though it is an extreme example.
End of conversation
New conversation -
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.