Do you want to define syntax with binders in Agda but have no idea whether to use de Bruijn indices, nominal sets, HOAS, or yet something else?
Well then, good news! I have a new blog post for you: jesper.sikanda.be/posts/1001-syn
4
40
133
Conversation
Super great overview, thanks for this! I'm still pretty happy with defunctionalized NbE (with indices in terms and levels in values). Makes implementation much easier, and is good for performance, but I dunno how it fares for formalization work.
3
6
The reason I mention it is that I wasted a lot of time with trying to use locally nameless, but it turns out NbE makes things so much easier when implementing type systems! I dunno if it would fit into your post anywhere though. 😅