[Agda] Termination checking (perhaps could be smarter)

[Carlos Camarao]

Thanks Gregor, I will install Agda 2.4.2!

Cheers,

Carlos

On Thu, Jan 15, 2015 at 4:07 PM, Gregor Ulm <gregor.ulm at gmail.com> wrote:
> 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
>>