```
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: Jun 20 2024 at 13:02 UTC