This is the definition from the standard library:

```
Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}.
Defined.
```

— What is going on here? I tried to dig up the `+`

in the Coq reference, but it is not easily searchable and I do not even know which chapter to look for it in… I understand that it must be a variant type of some sort?

`Locate "+"`

is what you want - or alternatively switch off the display of notations (in CoqIDE from the View Menu). `Locate "+"`

gives:

```
Notation "{ A } + { B }" := (sumbool A B) : type_scope (default interpretation)
Notation "A + { B }" := (sumor A B) : type_scope (default interpretation)
Notation "x + y" := (Nat.add x y) : nat_scope (default interpretation)
Notation "x + y" := (sum x y) : type_scope
```

Now you can do `Print sumbool.`

.

Oh, I see. I was assuming that this `+`

must be some sort of a built in notation. But it is actually defined somewhere else in the library, where `sumbool`

is actually defined as a sum type, as I thought it should be. Thanks!

Very little of the notations you see in Coq is built in. E.g. even "->" is a defined notation. IMHO it is fascinating that one can build complex theories from so little.

The built in stuff is here: (https://coq.inria.fr/refman/language/core/basic.html#essential-vocabulary).

Last updated: Jun 18 2024 at 22:01 UTC