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…
Trying to work up to doing proofs about system Fω and CoC-style stuff. Feeling muchly mentally underequipped. 😅
1
1
Replying to
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
Show replies