<div dir="ltr">Hi,<div><br></div><div>As far as I know, the issue is that </div><div><br></div><div>1. Agda elaborates pattern matching lambdas to new top-level definitions with machine-generated names</div><div>2. Agda does not look into bodies of pattern matching functions when checking definitional equality</div><div><br></div><div>Hence, Agda doesn't know that two pattern matching lambdas which look the same in the source are equal.</div><div><br></div><div>People tolerate this limitation because we rarely rely on the rather fragile intensional equality of functions. Instead we postulate function extensionality when required.</div><div><br></div><div>If you'd like to have a bit more intensional function equality, you can use top-level lemmas instead of pattern lambdas, <a href="http://lpaste.net/363727">like this</a>.</div><div><br></div><div>If you'd like to have as much as possible intensional function equality, you need to write all of your functions in terms of eliminators, thereby making all of your function bodies visible to Agda, as induction method arguments to eliminators.</div></div><div class="gmail_extra"><br><div class="gmail_quote">2018-03-17 18:59 GMT+01:00 Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Why does the attached not work? Is there a workaround, or a repair on the horizon? Note particularly the "1" in the error message, which appears spurious. Cheers, -- P<div><br clear="all"><div><div class="m_-6258484800341045637gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div></div></div></div></div>
</div></div>
<br>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>