[Agda] eta expansion

Nils Anders Danielsson nad at chalmers.se
Fri Mar 8 17:59:08 CET 2013

On 2013-03-08 16:37, Andreas Abel wrote:
> Without eta, the equation Y x == f x gives two different solutions for
> Y: f and \lambda x -> f x.  It is not clear which one Agda should
> choose, one of the tests would fail, and it would be rather arbitrary.

I think it's clear that Agda should refrain from choosing a solution.
This isn't arbitrary (but both tests would fail).


More information about the Agda mailing list