<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Consolas;
panose-1:2 11 6 9 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
pre
{mso-style-priority:99;
mso-style-link:"HTML Preformatted Char";
margin:0cm;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:"Consolas",serif;}
span.EmailStyle21
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="blue" vlink="purple" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Yes, you have to normalize all previous constraints when you add a new one.
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Thorsten<o:p></o:p></span></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="margin-bottom:12.0pt"><b><span style="font-size:12.0pt;color:black">From:
</span></b><span style="font-size:12.0pt;color:black">Agda <agda-bounces@lists.chalmers.se> on behalf of Andreas Nuyts <andreasnuyts@gmail.com><br>
<b>Date: </b>Thursday, 1 September 2022 at 12:09<br>
<b>To: </b>Thorsten Altenkirch (staff) <psztxa@exmail.nottingham.ac.uk>, Andrew Pitts <Andrew.Pitts@cl.cam.ac.uk>, agda@lists.chalmers.se <agda@lists.chalmers.se>, Miëtek Bak <mietek@bak.io><br>
<b>Subject: </b>Re: [Agda] Path to success with Agda?<o:p></o:p></span></p>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt">Hi,<br>
<br>
I've been thinking along the lines of this smart case proposal when wondering about the possibility of judgemental naturality (w.r.t. the motive) of eliminators.<br>
<br>
I think you have to be more careful when merging constraint sets: what if a new constraint n = b is added to a constraint set containing n' = b' where n' is blocked by the neutral subterm n? This situation doesn't seem to be addressed in the slides as they
are.<br>
<br>
Best,<br>
Andreas N<o:p></o:p></p>
<div>
<p class="MsoNormal">On 31.08.22 14:57, Thorsten Altenkirch wrote:<o:p></o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Maybe somebody should implement the smart case…
</span><o:p></o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><a href="http://www.cs.nott.ac.uk/~psztxa/talks/shonan11.pdf">http://www.cs.nott.ac.uk/~psztxa/talks/shonan11.pdf</a></span><o:p></o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="margin-bottom:12.0pt"><b><span style="font-size:12.0pt;color:black">From:
</span></b><span style="font-size:12.0pt;color:black">Agda <a href="mailto:agda-bounces@lists.chalmers.se">
<agda-bounces@lists.chalmers.se></a> on behalf of Andrew Pitts <a href="mailto:Andrew.Pitts@cl.cam.ac.uk">
<Andrew.Pitts@cl.cam.ac.uk></a><br>
<b>Date: </b>Tuesday, 30 August 2022 at 10:48<br>
<b>To: </b><a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a> <a href="mailto:agda@lists.chalmers.se">
<agda@lists.chalmers.se></a>, Miëtek Bak <a href="mailto:mietek@bak.io"><mietek@bak.io></a><br>
<b>Subject: </b>Re: [Agda] Path to success with Agda?</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><br>
<br>
> On 30 Aug 2022, at 09:29, Miëtek Bak <a href="mailto:mietek@bak.io"><mietek@bak.io></a> wrote:<br>
> <br>
>> On 30 Aug 2022, at 09:58, Andrew Pitts <a href="mailto:Andrew.Pitts@cl.cam.ac.uk">
<Andrew.Pitts@cl.cam.ac.uk></a> wrote:<br>
>> <br>
>> So I wanted to mention the humble “case” expression, which functional programmers can more easily relate to, maybe. It’s less powerful that “with”, but sometimes works (wrt the not typechecking thing) when “with” won’t.<br>
> <br>
> It would be interesting to see an example in which `case` works and `with` does not.<br>
<br>
I have some and will try to extract them from their context when I get a mo. However, I should qualify what I said:<br>
<br>
"but sometimes [case] works (wrt the not typechecking thing) when “with” won’t”<br>
<br>
What I really meant was that, at the time, it was easier for me to use a “case" expression than to figure out how to still use “with” by moving lemmas to the top level, generalizing arguments a bit more, etc, etc. I expect there’s always a way with “with”.
<br>
<br>
And if you are heavily in to using “rewrite” (“with” disguised), then I guess “case” is not helpful.<br>
<br>
Andy<br>
<br>
_______________________________________________<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">https://lists.chalmers.se/mailman/listinfo/agda</a><o:p></o:p></p>
</div>
<pre>This message and any attachment are intended solely for the addressee<o:p></o:p></pre>
<pre>and may contain confidential information. If you have received this<o:p></o:p></pre>
<pre>message in error, please contact the sender and delete the email and<o:p></o:p></pre>
<pre>attachment. <o:p></o:p></pre>
<pre><o:p> </o:p></pre>
<pre>Any views or opinions expressed by the author of this email do not<o:p></o:p></pre>
<pre>necessarily reflect the views of the University of Nottingham. Email<o:p></o:p></pre>
<pre>communications with the University of Nottingham may be monitored <o:p></o:p></pre>
<pre>where permitted by law.<o:p></o:p></pre>
<pre><o:p> </o:p></pre>
<pre><o:p> </o:p></pre>
<pre><o:p> </o:p></pre>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<pre>_______________________________________________<o:p></o:p></pre>
<pre>Agda mailing list<o:p></o:p></pre>
<pre><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><o:p></o:p></pre>
<pre><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><o:p></o:p></pre>
</blockquote>
<p class="MsoNormal"><o:p> </o:p></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></body>
</html>