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 …
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.
-
-
I think a big improvement to make on the current Idris elab refl is to bake-in quotations a la Eli Barzilay's thesis, rather than representing them as just another datatype. Something like data TT = ... | Quote Nat TT where the quote level 0 is an antiquotation
-
Can we also have IO side effects in Elab? (as mentioned in the conclusion section of
@d_christiansen's dissertation) For example, it would allow us to call an SMT solver inside Elab. - 1 more reply
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.