```
match l with
| nil => false
| l' => if (eqb_nat a b) then true else
match(f3 a b l') with
| nil =>false
```

In above (eqb_nat a b) is being applied on non empty case. Therefore it is applied on one element and more than one element.But i want to apply true case on single element and false case on two or more element. I introduced new matching pattern but get error message non exhaustive pattern matching.

I am modifying like this

```
match l with
| nil => false
| l' => match l' with
|[c]=> if (eqb_nat a b) then true else
|c1::c2::t=> (eqb_nat a b)=false then
match(f3 a b l') with
| nil =>false...
```

Here are two ways to check with pattern matching that a list has exactly two elements

```
Require Import List.
Import ListNotations.
Definition has_exactly_two_elements1 (l : list nat) :=
match l with
| nil => false (* zero element *)
| a :: nil => false (* one element *)
| a :: b :: nil => true (* exactly two *)
| a :: b :: c :: l => false (* at least three *)
end.
Definition has_exactly_two_elements2 (l : list nat) :=
match l with
| nil => false (* zero element *)
| a :: l1 => (* at least one *)
match l1 with
| nil => false (* one element *)
| b :: l2 => match l2 with (* at least two *)
| nil => true (* two elements *)
| c :: l3 => false (* at leas three *)
end
end
end.
```

in your second match, Coq does not recall that `l'`

is non-empty. You should write

```
match l with
| nil => false
| c1:: l' => match l' with
|nil => if (eqb_nat a b) then true else
|c2::t=> (eqb_nat a b)=false then
match(f3 a b l') with
```

Last updated: Jun 20 2024 at 11:02 UTC