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...
Conversation
Replying to
Ooh, what magic is this `%runElab` thingy? How does it know about those user-defined data types you made in that gist? Does it verify that they're of the right 'shape' first, or is it more of a macro-style thing?
Replying to
1
2
Oh right, cool! Think I've come across that one before!
1
1
Show replies