<div dir="ltr"><div>You can report it by clicking the "New Issue" button here: <a href="https://github.com/agda/agda/issues">https://github.com/agda/agda/issues</a><br><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Mar 17, 2018 at 9:28 PM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Thanks, that works! My final solution is attached.<div><br></div><div>The '1' that appears in printing the function body in my original message appears to be a bug, and should be fixed. If it's not on a list of known bugs, what would I do to add it?</div><div><br></div><div>Cheers, -- P</div></div><div class="gmail_extra"><span class=""><br clear="all"><div><div class="m_-8899465774334274986gmail_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>
<br></span><div><div class="h5"><div class="gmail_quote">On 17 March 2018 at 15:22, András Kovács <span dir="ltr"><<a href="mailto:kovacsahun@hotmail.com" target="_blank">kovacsahun@hotmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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" target="_blank">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"><div><div class="m_-8899465774334274986h5">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></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="m_-8899465774334274986h5"><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_-8899465774334274986m_2569299093537855027m_-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></div></div>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" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></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>