Type System & PL Twitter question:
What is a good name for the opposite of 'elaboration'? Ie. going from the core language back to the surface language. Some ideas:
- resugaring
- delaboration
- co-elaboration (collaboration? 🤪)
Conversation
In Agda it's called reification
1
2
Yeah I swear I originally got 'resugar' from somewhere in the agda source code, but I think I was using it in a different place. Might have been 'F*' though, come to think of it.

