Skip to main content

Questions tagged [eta-equality]

Things related to η-convertibility, η-expansion, η-reduction, and their use in simplifying proofs.

1 question with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
7 votes
0 answers
195 views

What was the first proof assistant with eta equality for records?

The Agda language supports eta equality for (non-(co)inductive) record types: ...
Jesper's user avatar
  • 506