Questions tagged [alpha-equivalence]

α-equivalence is used for renaming bound variables.

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
17 votes
2 answers

How to deal with Binders?

When reasoning about programming languages in a deep embedding, $\alpha$-equivalence, binders and capture-avoiding substitution quickly can become tedious. Complex binders may introduce multiple bound ...
Wno-all's user avatar
  • 1,108