De Bruijn indices are one of those things that never cease to turn my brain inside out any time I try to make sense of them 😖
Conversation
The basic idea or using them in practice or?
1
Implementing/using/writing proofs with
1
1
Notation wise they are all back-to-front. Seeing as the what the numbers refer to depends on the scoping. Super clever, but mind-bending…
2
I haven't had reason to try using either yet, but there's also de Bruijn *levels* which are the reverse, and count from the outside in.
1
(There is probably a reason why everyone uses indices and not levels though. At least, I assume.)
1
Replying to
Oh, they are different? That makes a ton more sense. I think indices are nice because its easier to prove type equivalence (it's just refl)