[Agda] Termination checking (perhaps could be smarter)

[Gregor Ulm]

Hello Carlos,

it seems that upgrading your Agda installation will solve your
problem. I'm using Agda 2.4.2, and the function 'sorted' does not get
highlighted as non-terminating when I type check your file.

Best regards,
Gregor

On Thu, Jan 15, 2015 at 6:55 PM, Carlos Camarao
<carlos.camarao at gmail.com> wrote:
> Hello.
>
> I am writing a simple insertion sort program in Agda, and proving its
> correctness. I am using the following predicate (the full code of the
> program is attached; I am using Agda version 2.3.2.2):
>
> sorted : List A → Bool
> sorted []           = true
> sorted (_ ∷ [])    = true
> sorted (a ∷ b ∷ x) with a ≤? b
> ... | yes _ = sorted (b ∷ x)
> ... | no  _ = false
>
> Agda hightlights the name of function sorted (in light salmon),
> indicating that it could not determine the function's termination. But argument
> (b ∷ x) is structurally smaller than (a ∷ b ∷ x), right? Any comments?
>
> Please feel free to send me also any other comments you think it is
> appropriate, related to the attached Agda code (for example related to
> module parameters).
>
> Regards,
>
> Carlos
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>