Fixpoint isSorted (l: list nat): bool :=
match l with
| nil => true
| x :: nil => true
| x1 :: x2 :: xs => if x1 <=? x2 then isSorted (x2 :: xs) else false
end.
the code throws error around isSorted (x2 :: xs)
. Why?
Is the error Cannot guess decreasing argument of fix ?
Even though it is clear for us that x2 :: xs
is a subterm of x1 :: x2 :: xs
, this is not clear for Coq. Here is how you can make it clear:
Fixpoint isSorted (l: list nat): bool :=
match l with
| nil => true
| x :: nil => true
| x1 :: (x2 :: xs) as x2xs => if x1 <=? x2 then isSorted x2xs else false
end.
That indeed solved the problem. Thanks!
Last updated: Oct 13 2024 at 01:02 UTC