Skip to main content

Questions tagged [de-bruijn-indexing]

For questions about De Bruijn indices or levels, an encoding method used to efficiently implement variable names with bindings.

Filter by
Sorted by
Tagged with
1 vote
1 answer

Alpha equivalent subgoals

I'm working on proof automation methods using Lean, and have noticed that quite often there will be many subgoals generated which are alpha-equivalent, which I would like to discard. For example, the ...
SAL's user avatar
  • 13
19 votes
1 answer

When should I use De Bruijn levels instead of indices?

I am familiar with De Bruijn indices, but not with De Bruijn levels. In my understanding, indices index variables from the top of the context/stack, whereas levels index variables from the bottom. So ...
Couchy's user avatar
  • 2,221