<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=utf-8">
<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;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.gmail-im
{mso-style-name:gmail-im;}
span.EmailStyle19
{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">
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">I guess this shouldn’t be just a checker but a way to prove externally that the system is terminating using agda.<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">T.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><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"><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 Jesper Cockx <Jesper@sikanda.be><br>
<b>Date: </b>Tuesday, 29 January 2019 at 14:42<br>
<b>To: </b>Nils Anders Danielsson <nad@cse.gu.se><br>
<b>Cc: </b>agda list <Agda@lists.chalmers.se><br>
<b>Subject: </b>Re: [Agda] Termination checker and rewriting<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal"><a name="_MailOriginalBody"><span class="gmail-im">On 29/01/2019 13.57, Guillaume GENESTIER wrote:</span></a><span style="mso-bookmark:_MailOriginalBody"><br>
<span class="gmail-im">> More specifically, I was wondering if any termination checking is</span><br>
<span class="gmail-im">> performed on these rules.</span><br>
<br>
No.<o:p></o:p></span></p>
</blockquote>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody">... but if you are interested in working on implementing a termination checker for rewrite rules, send me a mail and let's talk.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody">-- Jesper<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody"><o:p> </o:p></span></p>
<div>
<div>
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody">On Tue, Jan 29, 2019 at 2:19 PM Nils Anders Danielsson <</span><a href="mailto:nad@cse.gu.se"><span style="mso-bookmark:_MailOriginalBody">nad@cse.gu.se</span><span style="mso-bookmark:_MailOriginalBody"></span></a><span style="mso-bookmark:_MailOriginalBody">>
wrote:<o:p></o:p></span></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal"><span style="mso-bookmark:_MailOriginalBody">On 29/01/2019 13.57, Guillaume GENESTIER wrote:<br>
> More specifically, I was wondering if any termination checking is<br>
> performed on these rules.<br>
<br>
No.<br>
<br>
-- <br>
/NAD<br>
_______________________________________________<br>
Agda mailing list<br>
</span><a href="mailto:Agda@lists.chalmers.se" target="_blank"><span style="mso-bookmark:_MailOriginalBody">Agda@lists.chalmers.se</span><span style="mso-bookmark:_MailOriginalBody"></span></a><span style="mso-bookmark:_MailOriginalBody"><br>
</span><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank"><span style="mso-bookmark:_MailOriginalBody">https://lists.chalmers.se/mailman/listinfo/agda</span><span style="mso-bookmark:_MailOriginalBody"></span></a><span style="mso-bookmark:_MailOriginalBody"><o:p></o:p></span></p>
</blockquote>
</div>
</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>