<div dir="ltr"><div>Hi Thorsten,</div><div><br></div><div>'Let' statements are part of the term syntax of Agda and are desugared during typechecking (by inlining). In contrast, 'where' statements are part of the syntax for <i>declarations</i> so they cannot appear inside terms directly. Pattern matching is not part of the term syntax of Agda (unlike Coq where eliminators can appear in terms), so in general pattern matching can only happen at the declaration level. <br></div><div><br></div><div>The exception to this rule are pattern matching lambdas, which are actually implemented internally by lifting the whole expression to an (anonymous) top-level definition. It should probably be possible to extend let-expressions with the same trick. However, this would mean pattern-matching let's would be generative, i.e. two syntactically equal let-expressions might not be definitionally equal since they are desugared to two separate anonymous definitions internally.</div><div><br></div><div>Another more drastic solution would be to extend Agda's internal syntax with some kind of pattern-matching construct, e.g. eliminators or case trees. But this would basically require a complete overhaul of Agda's internals, so I do not expect this will happen in the forseeable future (perhaps it could be part of the mythical Agda 3.0).</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Feb 29, 2020 at 2:13 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">





<div lang="EN-GB">
<div class="gmail-m_-4823492196277812785WordSection1">
<p class="MsoNormal"><span style="font-size:11pt">Hi,<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">Can somebody remind me for what (historical ?) reasons “where” allows pattern matching but not “let”? What are the obstacles to fixing this?<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">Thanks,<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">Thorsten<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
</div>
<pre>This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.



</pre></div>

_______________________________________________<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/mailman/listinfo/agda</a><br>
</blockquote></div>