<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>