<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>I believe that you are right that the two snippets are
equivalent, but it requires some computation to show that this is
the case.<br>
The check that Agda runs on the other hand is very syntactic. This
is indeed a limitation, but at least it ensures that checking for
termination terminates ;-)<br>
<br>
</p>
<div class="moz-cite-prefix">On 07/30/2018 06:04 PM, Serge Leblanc
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:6cc7f922-8f49-df2d-c665-4e7e128d3b96@gmail.com">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
Yes, but you translat the code <font color="#3333ff">(toCostring
">>") ++ coSplit "(♭ xs)</font> to its normal form, it
equals to <font color="#3333ff">'>' ∷ ♯ ('>' ∷ ♯ coSplit
'(♭ xs))</font>. Right?<br>
So, the recursive call is well protected by a constructor.<br>
<br>
Jes, sed vi plenumas la kodon (toCostring ">>") ++ coSplit″
(♭ xs) ĝis sia normala formo, ĝi egalas al '>' ∷ ♯ ('>' ∷ ♯
coSplit′ (♭ xs)). Ĉu ne ?<br>
Do, la memsinkceva alvoko estas bone ŝirmi per konstruisto.<br>
<br>
<div class="moz-cite-prefix">On 2018-07-30 16:59, a.j.rouvoet
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:5f007898-9a15-5868-7882-bc70ea2546ed@gmail.com">
<meta http-equiv="Content-Type" content="text/html;
charset=utf-8">
<p>For coSplit to pass the checker, the recursive invocation
must appear guarded by a constructor.<br>
This is clearly the case in coSplit', but not necessarily in
coSplit'' (e.g. when toString ">>" returns the empty
costring).<br>
</p>
<br>
<div class="moz-cite-prefix">On 07/30/2018 04:55 PM, Serge
Leblanc wrote:<br>
</div>
<blockquote type="cite"
cite="mid:0961b22f-b45b-5827-1c60-9910534d45c1@gmail.com">
<meta http-equiv="content-type" content="text/html;
charset=utf-8">
<span id="result_box" class="" lang="en"><span class="">Dear
all,<br>
Why the checking termination rejects the coSplit" function
although the coSplit' function is accepted ?</span></span><br>
<span id="result_box" class="" lang="en"><span class=""><span
id="result_box" class="short_text" lang="en"><span
class=""><span id="result_box" class="" lang="en"><span
class="">Why the checking termination so
suspicious?</span></span><br>
</span></span>Sincerely<br>
</span></span><br>
Estimataj ĉiuj,<br>
Kial la finiĝa kontrolo malakceptas la funkcion coSplit″
kvankam la funkcio coSplit′ trafas ?<br>
Kial la finiĝa kontrolo estas tiel malakceptanda ?<br>
Sincere<br>
<br>
<font color="#3333ff"> coSplit′ : Costring → Costring<br>
coSplit′ [] = []<br>
coSplit′ (x ∷ xs) with x ≐ '!'<br>
... | false = x ∷ ♯ coSplit′ (♭ xs)<br>
... | true = '>' ∷ ♯ ('>' ∷ ♯ coSplit′ (♭ xs))<br>
<br>
coSplit″ : Costring → Costring<br>
coSplit″ [] = []<br>
coSplit″ (x ∷ xs) with x ≐ '!'<br>
... | false = x ∷ ♯ coSplit″ (♭ xs)<br>
... | true = (toCostring ">>") ++ coSplit″ (♭ xs)<br>
<br>
main = run $ ♯ getContents >>= λ s → ♯ (putStrLn∞ ∘
coSplit′) s<br>
<span id="result_box" class="" lang="en"><span class=""></span></span></font>
<div class="moz-signature"><font color="#3333ff"><br>
</font>-- <br>
Serge Leblanc
<hr> gpg --search-keys 0x67B17A3F <br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1
7A3F</div>
<!--'"--><br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" moz-do-not-send="true">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" moz-do-not-send="true">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
<div class="moz-signature">-- <br>
Serge Leblanc
<hr> gpg --search-keys 0x67B17A3F <br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
<!--'"--><br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>