Ignat Insarov (Mar 26 2021 at 08:18): 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