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