[Agda] Absurd lambdas and equality

[Ulf Norell]

On Tue, Jul 12, 2011 at 2:04 AM, Daniel Peebles <pumpkingod at gmail.com>wrote:

> I was wondering if someone could explain why two absurd lambdas of the same
> type are not equal. I've run into issues with this several times, when
> proving things about definitions that involve them, and am just curious what
> the motivation for this is.


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.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110712/c38b5c3b/attachment.html