diff options
Diffstat (limited to 'theories/Init/Datatypes.v')
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Datatypes.v | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 6aeabe13..f71f58c6 100755..100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -6,19 +6,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Datatypes.v,v 1.26.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) +(*i $Id: Datatypes.v 8642 2006-03-17 10:09:02Z notin $ i*) + +Set Implicit Arguments. Require Import Notations. Require Import Logic. -Set Implicit Arguments. - (** [unit] is a singleton datatype with sole inhabitant [tt] *) Inductive unit : Set := tt : unit. -(** [bool] is the datatype of the booleans values [true] and [false] *) +(** [bool] is the datatype of the boolean values [true] and [false] *) Inductive bool : Set := | true : bool @@ -27,7 +27,9 @@ Inductive bool : Set := Add Printing If bool. (** [nat] is the datatype of natural numbers built from [O] and successor [S]; - note that zero is the letter O, not the numeral 0 *) + note that the constructor name is the letter O. + Numbers in [nat] can be denoted using a decimal notation; + e.g. [3%nat] abbreviates [S (S (S O))] *) Inductive nat : Set := | O : nat @@ -53,7 +55,7 @@ Implicit Arguments identity_ind [A]. Implicit Arguments identity_rec [A]. Implicit Arguments identity_rect [A]. -(** [option A] is the extension of A with a dummy element None *) +(** [option A] is the extension of [A] with an extra element [None] *) Inductive option (A:Set) : Set := | Some : A -> option A @@ -61,7 +63,13 @@ Inductive option (A:Set) : Set := Implicit Arguments None [A]. -(** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *) +Definition option_map (A B:Set) (f:A->B) o := + match o with + | Some a => Some (f a) + | None => None + end. + +(** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *) (* Syntax defined in Specif.v *) Inductive sum (A B:Set) : Set := | inl : A -> sum A B |