## Stream: Coq users

### Topic: What is `+` in `sumbool`?

#### Ignat Insarov (Mar 26 2021 at 08:18):

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?

#### Michael Soegtrop (Mar 26 2021 at 08:22):

`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.`.

#### Ignat Insarov (Mar 26 2021 at 08:31):

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!

#### Michael Soegtrop (Mar 26 2021 at 08:49):

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: Oct 03 2023 at 04:02 UTC