Questions tagged [alpha-equivalence]
α-equivalence is used for renaming bound variables.
2
questions
1
vote
1
answer
66
views
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 ...
- 13
18
votes
2
answers
398
views
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 ...
- 1,128