Questions tagged [eta-conversion]
An η-reduction rule describes how to reduce a term that involves a constructor applied to an eliminator. For example, in the lambda calculus, the term λx.(t x) reduces to t. Two terms are η-convertible when they are identical up to a sequence of η-reductions.
1
question
13
votes
2
answers
292
views
Is eta-equality provable in Coq?
Trying to answer another question, I can't help second guessing myself about whether eta equality is provable in Coq. In particular, can one prove
...
- 2,061