<br><div class="gmail_quote">On Tue, Jul 12, 2011 at 2:04 AM, Daniel Peebles <span dir="ltr"><<a href="mailto:pumpkingod@gmail.com">pumpkingod@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
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.</blockquote>
<div><br></div><div>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.</div><div>
<br>
</div><div>/ Ulf </div></div>