<div dir="ltr">That is weird. I don't have any concrete suggestions apart from the one you've already mentioned, apologies, but I'd definitely advise filing a bug report on the Agda repo.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Aug 20, 2021 at 6:45 AM Jason Hu <<a href="mailto:fdhzs2010@hotmail.com">fdhzs2010@hotmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">





<div lang="EN-US" style="overflow-wrap: break-word;">
<div class="gmail-m_3246457612591460909WordSection1">
<p class="MsoNormal">Hi all,</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">It sounds like a stupid question but it seems to me there isn’t a convenient way to do it. What I want to do is to do induction on a non-empty list as defined in the stdlib in a “standard” way. To illustrate the problem, consider the following
 program:</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">open import Data.Nat<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">open import Data.List<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">open import Data.List.NonEmpty<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New""><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">len : List</span><span style="font-family:"Cambria Math",serif">⁺</span><span style="font-family:"Courier New"">
</span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""> →
</span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""><u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">len (x </span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""> []) = 1<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">len (x </span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""> y
</span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""> l) = len (y
</span><span style="font-family:"Cambria Math",serif">∷</span><span style="font-family:"Courier New""> l)<u></u><u></u></span></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">As of 2.6.2, Agda doesn’t like this definition and complains that len does not terminate. What I am looking for is a solution that does not require defining a “helper” which handle the underlying list, and the “main” function which does
 the job separately.</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Any idea is appreciated.</p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Thanks,<u></u><u></u></p>
<p class="MsoNormal">Jason Hu<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>

_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>