Things related to η-convertibility, η-expansion, η-reduction, and their use in simplifying proofs.
In type theory, η-conversion is a process of “computation” which is “dual” to beta-conversion.
The equivalence relation generated by η-reduction/expansion is called η-equivalence, and the whole collection of processes is called η-conversion.
(from nLab)
References:
η-conversion (nLab)
|
created |
2 years, 5 months ago |
|
viewed |
8 times |
|
active |
2 years, 5 months ago |
|
editors |
1 |
