<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
Thank you for your help.
<p>Why Agda refuses the following structurally decreasing function?
<br>
</p>
foldl″ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A<br>
foldl″ c (n ∷ []) = n<br>
foldl″ c (n ∷ (x ∷ xs)) = foldl″ c (c n x ∷ xs)<br>
<br>
<span style="color: rgb(157, 165, 180); font-family: inconsolata, Menlo, Consolas, "DejaVu Sans Mono", "Liberation Mono", Monaco, "Lucida Console", monospace; font-size: 15px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; line-height: 30px; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: pre-wrap; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; display: inline !important; float: none; background-color: rgb(33, 37, 43);">/home/serge/agda/Maximal.agda:47,1-49,50
Termination checking failed for the following functions:
foldl″
Problematic calls:
foldl″ c (c n x ∷ xs)
(at /home/serge/agda/Maximal.agda:49,27-33)</span><br>
<br>
<div class="moz-cite-prefix">On 2017-08-14 20:55, Ulf Norell wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAJjNqYF=GadEsT3zEjseAc7ChhqkVF_MZBkjUphtBZB6yzmK3g@mail.gmail.com">
<div dir="ltr">The fact that <span style="font-size:12.8px">foldr₁</span> is
using a private recursive helper function will likely make it
impossible to prove your theorem.
<div><br>
</div>
<div>/ Ulf</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Mon, Aug 14, 2017 at 6:47 PM, Jesper
Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be"
target="_blank" moz-do-not-send="true">Jesper@sikanda.be</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">
<div>
<div>
<div>Maybe you can explain what approaches you have
already tried and why you got stuck? I think people
would be more inclined to help that way.<br>
<br>
</div>
To get you started on proof1, here's a hint: since you
are proving something about the functions foldr₁ and
_⊔_, you can take a look at their definitions and
follow the same structure for your proof. For example,
since foldr₁ is defined in terms of the helper
function foldr, you probably also need to define a
helper lemma that proves a similar statement about
foldr.<br>
<br>
</div>
Best regards,<br>
</div>
Jesper<br>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">
<div>
<div class="h5">2017-08-14 18:33 GMT+02:00 Serge
Leblanc <span dir="ltr"><<a
href="mailto:33dbqnxpy7if@gmail.com"
target="_blank" moz-do-not-send="true">33dbqnxpy7if@gmail.com</a>></span>:<br>
</div>
</div>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>
<div class="h5">
<div text="#000000" bgcolor="#FFFFFF">
<p>Saluton, neniu bonvolas helpi min?<br>
</p>
<p>Hi, nobody wants to help me?<br>
</p>
<div>
<div class="m_-5624432948826885329h5"> <br>
<div
class="m_-5624432948826885329m_-5308586550852440085moz-cite-prefix">On
2017-08-06 18:23, Serge Leblanc wrote:<br>
</div>
<blockquote type="cite"> <span
id="m_-5624432948826885329m_-5308586550852440085result_box"
lang="en"><span>Dear All,</span><br>
<span>I need help to finish these
lemmas.</span><br>
<span>They have the same meaning, I am
right?</span><br>
<span>All helpers are welcome!</span></span><br>
<br>
Estimata ĉiuj, <br>
Mi bezonas helpon por daŭrigi ci-tiuj
pruvojn!<br>
<div
class="m_-5624432948826885329m_-5308586550852440085moz-signature">Ĉu
ili havas je la saman signifon! Ĉu mi
pravas?<br>
Ĉiuj helpantoj estas bonvenaj!<br>
<br>
Sincere.<br>
-- <br>
Serge Leblanc
<hr> gpg --search-keys 0x67B17A3F <br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2
C2D3 B67C F631 67B1 7A3F</div>
</blockquote>
<br>
<div
class="m_-5624432948826885329m_-5308586550852440085moz-signature">--
<br>
Serge Leblanc
<hr> gpg --search-keys 0x67B17A3F <br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2
C2D3 B67C F631 67B1 7A3F</div>
</div>
</div>
</div>
<br>
</div>
</div>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se"
target="_blank" moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a
href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank"
moz-do-not-send="true">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
</blockquote>
</div>
<br>
</div>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br>
</blockquote>
</div>
<br>
</div>
</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>
</body>
</html>