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 …
-
-
The Lean folks made their similar feature really fast, it might be worth stealing some implementation techniques
-
My hunch is that the overhead will be quite small for what I have in mind (I'm only reflecting high level things for now) but once it gets to developing proof scripts I should certainly do that.
- 3 more replies
New conversation -
-
-
Just been starting to look at what is out there about structural dependent record types actually… there's some stuff out there by Luo and Feng. They base their stuff on LF which is a little alien after starting off with LambdaPi and Agda. So many weird ways of chopping up TT.

-
Do most folks just forgo structural records at the moment because the subtyping is really annoying?
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.