Expand description
Indices.
We find it useful to distinguish between backward indices (used in syntax, where 0 refers to the end of the context) and forward indices (used in values, where 0 refers to the beginning of the context).
In the literature, backward indices are known as DeBruijn indices and forward
indices are known as DeBruijn levels, but we think that “backwards and forwards”
is more clear, and it corresponds with “backwards and forwards linked lists”. A forwards linked list uses cons to put a new element on the front; a backwards
linked list uses snoc to put a new element on the back.
We take this terminology from narya.