<div dir="ltr"><div>I have a function that I believe terminates but Agda disagrees.</div><div><br></div><div><span style="font-family:monospace">hasDoubleLetter : List Char â†’ Bool<br>hasDoubleLetter [] = false<br>hasDoubleLetter (c₁ âˆ· cs@(câ‚‚ âˆ· _)) with c₁ == câ‚‚<br>... | yes _ = true<br>... | no Â _ = hasDoubleLetter cs    -- This is problematic.<br>hasDoubleLetter (_ âˆ· []) = false</span></div><div><br></div><div>Because `hasDoubleLetter` is recursively applied to a "smaller" structure (cs), I think it should be considered terminating. Am I missing something?<br></div><div><br></div><div>FWIW the error message is like below.</div><div><br></div><div><span style="font-family:monospace">Termination checking failed for the following functions:<br>  hasDoubleLetter<br>Problematic calls:<br>  hasDoubleLetter (c₁ âˆ· câ‚‚ âˆ· xs) | (EqChar Eq.== c₁) câ‚‚<br>  hasDoubleLetter (câ‚‚ âˆ· xs)<br></span><br></div></div>