I've recently started using Coq and after following and completing some tutorials I realized that I still know nothing. I've got the following code:

```
Require Import List.
Inductive Square := B | W | E.
Definition count_black (l : list Square) : nat :=
count_occ eq l B.
```

And it gives me the following error:

```
Error:
In environment
l : list Square
The term "eq" has type "?A0 -> ?A0 -> Prop" while it is expected to have type "forall x y : ?A, {x = y} + {x <> y}".
```

I've seen this {x = y} + {x <> y} before but I don't know what it means exactly, and more importantly how to get such an equality function for my custom type.

Can anyone help me out?

```
Require Import List.
Inductive Square := B | W | E.
Definition Square_eq_dec (x y : Square) : {x = y} + {x <> y}.
Proof. decide equality. Defined.
Definition count_black (l : list Square) : nat :=
count_occ Square_eq_dec l B.
```

A value of type `{ A } + { B }.`

contains either a proof of `A`

, or a proof of `B`

(see inductive definition below, if it helps) — here, value of type `{x = y} + {x <> y}`

are either proofs that `x = y`

or that `x <> y`

, and `Square_eq_dec`

is a function that takes arguments `x : Square`

and `y : Square`

and _decides_ whether they're equal or not — that is, it computes and returns a proof that they're equal, or a proof that they're not.

The following is more formal, but it might not make sense yet depending on the tutorials. Formally, `{ A } + { B }`

is a notation for type `sumbool`

:

```
Locate "{ _ } + { _ }".
(*
Notation "{ A } + { B }" := (sumbool A B) : type_scope
(default interpretation)
*)
```

and `sumbool`

is defined as the following inductive type:

```
Print sumbool.
(*
Inductive sumbool (A B : Prop) : Set :=
left : A -> {A} + {B} | right : B -> {A} + {B}.
*)
```

Thank you for your help. It seems to work now!

Last updated: Jun 23 2024 at 23:01 UTC