[Agda] Why is this non-terminating?

[James Wood]

Hi Jinwoo,

It looks fine to me, so this is probably some sort of bug / lack of
feature. Some easy things to test would be:

1. Remove the @-pattern, so the pattern is `(c₁ ∷ c₂ ∷ cs)`, and the
recursive call is on `c₂ ∷ cs`.
2. Remove the `with`, and instead find a way to go via `if_then_else_`.

Best,
James

On 03/07/2020 20:57, Jinwoo Lee wrote:
> I have a function that I believe terminates but Agda disagrees.
> 
> hasDoubleLetter : List Char → Bool
> hasDoubleLetter [] = false
> hasDoubleLetter (c₁ ∷ cs@(c₂ ∷ _)) with c₁ == c₂
> ... | yes _ = true
> ... | no  _ = hasDoubleLetter cs    -- This is problematic.
> hasDoubleLetter (_ ∷ []) = false
> 
> Because `hasDoubleLetter` is recursively applied to a "smaller"
> structure (cs), I think it should be considered terminating. Am I
> missing something?
> 
> FWIW the error message is like below.
> 
> Termination checking failed for the following functions:
>   hasDoubleLetter
> Problematic calls:
>   hasDoubleLetter (c₁ ∷ c₂ ∷ xs) | (EqChar Eq.== c₁) c₂
>   hasDoubleLetter (c₂ ∷ xs)
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>