Stream: Coq users

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


view this post on Zulip 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?

view this post on Zulip 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..

view this post on Zulip 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!

view this post on Zulip 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: Feb 04 2023 at 22:29 UTC