diff options
Diffstat (limited to 'theories/Init/Datatypes.v')
-rw-r--r-- | theories/Init/Datatypes.v | 49 |
1 files changed, 34 insertions, 15 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index f71f58c6..fdd7ba35 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Datatypes.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Datatypes.v 8872 2006-05-29 07:36:28Z herbelin $ i*) Set Implicit Arguments. @@ -47,7 +47,7 @@ Inductive Empty_set : Set :=. member is the singleton datatype [identity A a a] whose sole inhabitant is denoted [refl_identity A a] *) -Inductive identity (A:Type) (a:A) : A -> Set := +Inductive identity (A:Type) (a:A) : A -> Type := refl_identity : identity (A:=A) a a. Hint Resolve refl_identity: core v62. @@ -57,13 +57,13 @@ Implicit Arguments identity_rect [A]. (** [option A] is the extension of [A] with an extra element [None] *) -Inductive option (A:Set) : Set := +Inductive option (A:Type) : Type := | Some : A -> option A | None : option A. Implicit Arguments None [A]. -Definition option_map (A B:Set) (f:A->B) o := +Definition option_map (A B:Type) (f:A->B) o := match o with | Some a => Some (f a) | None => None @@ -71,7 +71,7 @@ Definition option_map (A B:Set) (f:A->B) o := (** [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 := +Inductive sum (A B:Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. @@ -80,7 +80,7 @@ Notation "x + y" := (sum x y) : type_scope. (** [prod A B], written [A * B], is the product of [A] and [B]; the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) -Inductive prod (A B:Set) : Set := +Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. Add Printing Let prod. @@ -88,31 +88,38 @@ Notation "x * y" := (prod x y) : type_scope. Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. Section projections. - Variables A B : Set. - Definition fst (p:A * B) := match p with - | (x, y) => x - end. - Definition snd (p:A * B) := match p with - | (x, y) => y - end. + Variables A B : Type. + Definition fst (p:A * B) := match p with + | (x, y) => x + end. + Definition snd (p:A * B) := match p with + | (x, y) => y + end. End projections. Hint Resolve pair inl inr: core v62. Lemma surjective_pairing : - forall (A B:Set) (p:A * B), p = pair (fst p) (snd p). + forall (A B:Type) (p:A * B), p = pair (fst p) (snd p). Proof. destruct p; reflexivity. Qed. Lemma injective_projections : - forall (A B:Set) (p1 p2:A * B), + forall (A B:Type) (p1 p2:A * B), fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2. Proof. destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd. rewrite Hfst; rewrite Hsnd; reflexivity. Qed. +Definition prod_uncurry (A B C:Type) (f:prod A B -> C) + (x:A) (y:B) : C := f (pair x y). + +Definition prod_curry (A B C:Type) (f:A -> B -> C) + (p:prod A B) : C := match p with + | pair x y => f x y + end. (** Comparison *) @@ -127,3 +134,15 @@ Definition CompOpp (r:comparison) := | Lt => Gt | Gt => Lt end. + +(* Compatibility *) + +Notation prodT := prod (only parsing). +Notation pairT := pair (only parsing). +Notation prodT_rect := prod_rect (only parsing). +Notation prodT_rec := prod_rec (only parsing). +Notation prodT_ind := prod_ind (only parsing). +Notation fstT := fst (only parsing). +Notation sndT := snd (only parsing). +Notation prodT_uncurry := prod_uncurry (only parsing). +Notation prodT_curry := prod_curry (only parsing). |