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 …
-
-
This is super cool! Got any more details to share on how to achieve this?
-
Main things are: metavariables are mutually defined global definitions, so preserve sharing; context as IO array so constant time lookup; glued representation of terms, so only normalising when strictly needed. Though who knows, it may all fall apart when scaled up...
- 5 more replies
New conversation -
-
-
Cool! Should let
@andrasKovacs6 know the good news! I still need to figure out metavariable solving, so I've not run into the fun of these performance problems yet!
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.