[Agda] eta expansion

[Nils Anders Danielsson]

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).

-- 
/NAD