# Troubleshooting

This page is intended to have short snippets of common errors in Agda code, and how to fix these.

## Termination checking and nested with

The function `isSorted` takes a list and maybe produces a witness that list is sorted.

```  isSorted : (xs : List ℕ) → Option (Sorted xs)
isSorted (x ∷ x' ∷ xs) with isLt x x'
isSorted (x ∷ x' ∷ xs) | None = None
isSorted (x ∷ x' ∷ xs) | Some a   with isSorted (x' ∷ xs)
isSorted (x ∷ x' ∷ xs) | Some a        | None = None
isSorted (x ∷ x' ∷ xs) | Some xSmaller | Some restSorted = Some (cons xSmaller restSorted)
isSorted (x ∷ []) = Some singleton
isSorted [] = Some empty
```

Agdas termination checker can't see that this termination check. The reason is how the with construct is desugared, it will internally create an auxiliary function and call this.

```  isSorted (x ∷ x' ∷ xs) = isSorted-aux x x' xs (isLt x x')
```

This auxiliary function will itself create one more (since we have a nested with) this time we have:

```  isSorted' x x' xs (Some a) = isSorted'' x x' xs a (isSorted (x' ∷ xs))
```

This call is not structurally smaller and Agdas termination checker complains. The solution is to make the recursive call earlier.

```  isSorted : (xs : List ℕ) → Option (Sorted xs)
isSorted (x ∷ x' ∷ xs) with isLt x x'  | isSorted (x' ∷ xs)
isSorted (x ∷ x' ∷ xs) | None          | _    = None
isSorted (x ∷ x' ∷ xs) | Some xSmaller | None = None
isSorted (x ∷ x' ∷ xs) | Some xSmaller | Some restSorted = Some (cons xSmaller restSorted)
isSorted (x ∷ []) = Some singleton
isSorted [] = Some empty
```