[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