Myself and noticed a correspondence like:
fwd-list ~ debruijn indices
bwd-list ~ debruijn levels
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Conversation
In well-scoped terms, I think you get something like the following:
read image description
ALT
2
5
Neat! I've notices the 'swap' behaviour of the weird integer arithmetic that seems only ever to be mentioned in passing, and tried to make APIs with last/prev for levels and first/next for indices but this is nice way of putting it.
1
2
I'll add forward/backward indices to my list of alternate names for debruijn levels/indices (which never really give any hints as to what they actually *do* 😅).
In the past I've tried these names for levels/indices respectively:
- global var/local var
- var id/var offset
1
3
I also find it interesting how the 'size' in quotation etc., behaves a bit like an erased/abstract environment? Have been tempted to make a type called `ErasedEnv` in the past (or more accurately, rename my `EnvLen` type to that).
2