Which proof assistants use de Bruijn indices internally to implement variable binding?
Conversation
Replying to
I'm pretty sure that:
- Lean uses locally nameless
- Idris 2 uses indices in terms and levels in values (as part of an implementation of NbE)