<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
I guess a rule of thumb is to provide a clear indication of the decreasing structure syntactically in order to please termination checker. There aren't many reasons why such check fails, so I personally don't find it's too bad. Though, I do wish I can specify
what is the decreasing structure in some occasions.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a target="_blank"></a></b></span></span></font> </div>
</div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Sergei Meshveliani <mechvel@botik.ru><br>
<b>Sent:</b> September 24, 2018 8:50 AM<br>
<b>To:</b> agda@lists.chalmers.se<br>
<b>Subject:</b> [Agda] two questions on type checker</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">Dear Agda developers<br>
<br>
I have two notes on a code of kind<br>
<br>
----------------------------------------------------<br>
lemma' y (x ∷ x' ∷ xs) _ i@(suc k , 1+k<|xx'xs|) =<br>
begin<br>
... <br>
lookup' (x' ∷ xs) (k , k<|x'xs|)<br>
≡⟨ lemma' y x'xs 0<|x'xs| (k , k<|x'xs|)<br>
...<br>
where<br>
x'xs = x' ∷ xs<br>
...<br>
----------------------------------------------------<br>
<br>
Agda 2.6.0-05e8112 reports<br>
<br>
-----------------<br>
Termination checking failed for the following functions:<br>
lemma'<br>
Problematic calls:<br>
lemma' y (x'xs y x x' xs x₁ k 1+k<|xx'xs|)<br>
(0<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)<br>
(k , k<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)<br>
...<br>
------------------<br>
<br>
First, the print-out of the lemma' call in the message differs greatly<br>
from the source code. Blanks inserted into identifiers, `∷' skipped etc.<br>
<br>
Second, with expanding x'xs to (x' ∷ xs) in the recursive call, Agda<br>
sees termination.<br>
Many users will not guess to do this expansion and will spend effort<br>
trying to provide a wise termination proof.<br>
If it is problematic to fix the feature, may be, Agda could issue some<br>
hints after the message about termination - ?<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</body>
</html>