[Agda] Termination checking (perhaps could be smarter)

[Carlos Camarao]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: insertionSort.agda
Type: application/octet-stream
Size: 1882 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150115/e7e84a32/insertionSort.obj