<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.25in 1.0in 1.25in;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-US" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">Hi all,</p>
<p class="MsoNormal"><o:p> </o:p></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"><o:p> </o:p></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">open import Data.Nat<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">open import Data.List<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">open import Data.List.NonEmpty<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New""><o:p> </o:p></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""><o:p></o:p></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<o:p></o:p></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)<o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></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"><o:p> </o:p></p>
<p class="MsoNormal">Any idea is appreciated.</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
<p class="MsoNormal">Jason Hu<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>