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.

Filter by
Sorted by
Tagged with
13 votes
2 answers

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 ...
Couchy's user avatar
  • 2,061