[Agda] Absurd lambdas and equality

Nils Anders Danielsson nad at chalmers.se
Tue Jul 12 10:06:55 CEST 2011


On 2011-07-12 08:09, Ulf Norell wrote:
> The reason is that absurd lambdas are desugared into helper functions
> with a single absurd clause. Different absurd lambdas translate into
> different helper functions and are thus not equal.

We have considered using proper α-equality for functions. Maybe some
time in the future.

-- 
/NAD



More information about the Agda mailing list