<div dir="ltr">Out of curiosity why is the library's nonempty length not what you want? Maybe there is another approach.<div><br></div><div><font color="#000000">One observation is that there is some sneakiness in the <span style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures">∷, </span>this program is:</font></div><div><br></div>





<p class="gmail-p1" style="margin:0px;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:Menlo;color:rgb(92,32,255)"><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,205);background-color:rgb(253,158,116)">len</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">:</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s4" style="font-variant-ligatures:no-common-ligatures">Data.List.NonEmpty.List⁺</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s4" style="font-variant-ligatures:no-common-ligatures">ℕ</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">→</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s4" style="font-variant-ligatures:no-common-ligatures">ℕ</span></p>
<p class="gmail-p2" style="margin:0px;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:Menlo;color:rgb(57,164,40)"><span class="gmail-s5" style="font-variant-ligatures:no-common-ligatures;color:rgb(92,32,255)">len</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">(</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)">x </span><span class="gmail-s4" style="font-variant-ligatures:no-common-ligatures">Data.List.NonEmpty.∷</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s4" style="font-variant-ligatures:no-common-ligatures">Data.List.[]</span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">)</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">=</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s6" style="font-variant-ligatures:no-common-ligatures;color:rgb(212,34,255)">1</span></p>
<div><span class="gmail-s5" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(92,32,255)">len</span><span class="gmail-s2" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">(</span><span class="gmail-s2" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)">x </span><span class="gmail-s4" style="color:rgb(57,164,40);font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures">Data.List.NonEmpty.∷</span><span class="gmail-s2" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> y </span><span class="gmail-s4" style="color:rgb(57,164,40);font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures">Data.List.∷</span><span class="gmail-s2" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> l</span><span class="gmail-s3" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">)</span><span class="gmail-s2" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">=</span><span class="gmail-s2" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s1" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(0,0,205);background-color:rgb(253,158,116)">len</span><span class="gmail-s2" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">(</span><span class="gmail-s2" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)">y </span><span class="gmail-s4" style="color:rgb(57,164,40);font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures">Data.List.NonEmpty.∷</span><span class="gmail-s2" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> l</span><span class="gmail-s3" style="font-family:Menlo;font-size:11px;font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">)</span> </div><div><br></div><div>So the RHS is not "obviously" smaller because it's a different constructor than the pattern match. The system is missing that there's a semantic relationship between the two cons'es that we see intuitively.</div><div><br></div><div>This pattern does work when the constructors match:</div><div><br></div><div>





<p class="gmail-p1" style="margin:0px;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:Menlo;color:rgb(92,32,255)"><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures">len2</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">:</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures">Data.List.List</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures">ℕ</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">→</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures">ℕ</span></p>
<p class="gmail-p2" style="margin:0px;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:Menlo;color:rgb(57,164,40)"><span class="gmail-s4" style="font-variant-ligatures:no-common-ligatures;color:rgb(92,32,255)">len2</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">(</span><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures">Data.List.[]</span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">)</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">=</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s5" style="font-variant-ligatures:no-common-ligatures;color:rgb(212,34,255)">0</span></p>
<p class="gmail-p2" style="margin:0px;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:Menlo;color:rgb(57,164,40)"><span class="gmail-s4" style="font-variant-ligatures:no-common-ligatures;color:rgb(92,32,255)">len2</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">(</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)">x </span><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures">Data.List.∷</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures">Data.List.[]</span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">)</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">=</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s5" style="font-variant-ligatures:no-common-ligatures;color:rgb(212,34,255)">1</span></p>
<p class="gmail-p2" style="margin:0px;font-variant-numeric:normal;font-variant-east-asian:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:Menlo;color:rgb(57,164,40)"><span class="gmail-s4" style="font-variant-ligatures:no-common-ligatures;color:rgb(92,32,255)">len2</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">(</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)">x </span><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures">Data.List.∷</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> y </span><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures">Data.List.∷</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> l</span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">)</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">=</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s5" style="font-variant-ligatures:no-common-ligatures;color:rgb(212,34,255)">1</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s4" style="font-variant-ligatures:no-common-ligatures;color:rgb(92,32,255)">+</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s4" style="font-variant-ligatures:no-common-ligatures;color:rgb(92,32,255)">len2</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">(</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)">y </span><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures">Data.List.∷</span><span class="gmail-s2" style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> l</span><span class="gmail-s3" style="font-variant-ligatures:no-common-ligatures;color:rgb(98,98,98)">)</span></p></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Aug 19, 2021 at 7:08 PM Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com">matthewdaggitt@gmail.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 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" target="_blank">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">
<div>
<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>
_______________________________________________<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>