```
Fixpoint eq (a b n1 n2: nat):bool:=
match a, b with
c1 , x1 => match c1 with
| 0 => match x1 with
Z (d) => if leb d n1 then true else false
| 1 => match x1 with
Z (d')=> if leb d' n2 then true else false
end
end
end.
```

Three time end is use for each case of c1?

You need to close a match before starting the next case of a match above it

```
Fixpoint eq (a b n1 n2: nat):bool:=
match a, b with
c1 , x1 => match c1 with
| 0 => match x1 with
Z (d) => if leb d n1 then true else false
end
| 1 => match x1 with
Z (d')=> if leb d' n2 then true else false
end
end
end.
```

You should indent your code properly. A `match`

expression in Coq must always be concluded by an `end`

(unlike in ocaml for instance).

```
Fixpoint eq (a b n1 n2 : nat) : bool :=
match a, b with
| c1 , x1 =>
match c1 with
| 0 =>
match x1 with
| Z d => if leb d n1 then true else false
end
| 1 =>
match x1 with
| Z d' => if leb d' n2 then true else false
end
end
end.
```

Also the first `match`

is useless as it only renames `a`

and `b`

to `c1`

and `x1`

respectively.

Thanks for correction.

I also use Théo's style of indenting `match`

, but it's not universal in the Coq community. (e.g., MathComp favors one-liners with a special notation `if c1 is 0 then ...`

)

```
Fixpoint eq (a b n1 n2 : nat) : bool :=
match a, b with
| c1 , x1 =>
match c1 with
| 0 =>
match x1 with
| Z d => or (leb d n1)(leb d n2)
end
| 1 =>
match x1 with
| Z d' => or (leb d' n2) (leb d' n1)
end
end
end.
```

Return type is still bool then why I get message " it is expected to have type "Prop".

Is `or`

of return type `bool`

? I guess not and you meant `orb`

?

orb

You wrote `or`

.

Ok ,ok thank you. If I write any lemma which explain the behavior of above function ,then I have to write first whether c=0 or 1 then write second parameter then any output. Can you write any lemma about above?

I don't understand what is `Z`

in your code. Is it a typo for `S`

?.

Or did you load any library (it would be useful to tell which one, or include your declaration of `Z`

in the code you send.

Let's assume it's a typo (perhaps you should have sent us an exact copy of your example).

```
Notation Z := S.
Fixpoint eq (a b n1 n2 : nat) : bool :=
match a, b with
| c1 , x1 =>
match c1 with
| 0 =>
match x1 with
| Z d => orb (leb d n1)(leb d n2)
end
| 1 =>
match x1 with
| Z d' => orb (leb d' n2) (leb d' n1)
end
end
end.
(*
Error: Non exhaustive pattern-matching: no clause found for pattern 0
*)
```

In Coq, pattern-matchings should be exhaustive, which is not the case of your `match x1`

.

You should add a clause `0 => ...`

to both of your pattern-matching.

I'm not sure to answer your last question, but a typical exhaustive, non-ambiguous pattern-matching on `nat`

can be as follows:

```
Fixpoint f (n:nat) : nat :=
match n with
0 => 33
| 1 => 42
| S (S p) => f p
end.
```

Last updated: Jun 15 2024 at 05:01 UTC