<div dir="ltr"><div>Thanks, James. Removing the @-pattern didn't affect anything. But replacing `with` with `if_then_else_` fixes it. Seems like a compiler bug.</div><div><br></div><div>Cheers</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jul 3, 2020 at 1:07 PM James Wood <<a href="mailto:james.wood.100@strath.ac.uk">james.wood.100@strath.ac.uk</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">Hi Jinwoo,<br>
<br>
It looks fine to me, so this is probably some sort of bug / lack of<br>
feature. Some easy things to test would be:<br>
<br>
1. Remove the @-pattern, so the pattern is `(c₁ ∷ c₂ ∷ cs)`, and the<br>
recursive call is on `c₂ ∷ cs`.<br>
2. Remove the `with`, and instead find a way to go via `if_then_else_`.<br>
<br>
Best,<br>
James<br>
<br>
On 03/07/2020 20:57, Jinwoo Lee wrote:<br>
> I have a function that I believe terminates but Agda disagrees.<br>
> <br>
> 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<br>
> <br>
> Because `hasDoubleLetter` is recursively applied to a "smaller"<br>
> structure (cs), I think it should be considered terminating. Am I<br>
> missing something?<br>
> <br>
> FWIW the error message is like below.<br>
> <br>
> 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>
> <br>
> <br>
> _______________________________________________<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>
> <br>
_______________________________________________<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>