diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /theories/Init/Logic_Type.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'theories/Init/Logic_Type.v')
-rw-r--r--[-rwxr-xr-x] | theories/Init/Logic_Type.v | 62 |
1 files changed, 34 insertions, 28 deletions
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 0e62e842..857ffe94 100755..100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -6,18 +6,48 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Logic_Type.v,v 1.19.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) +(*i $Id: Logic_Type.v 8642 2006-03-17 10:09:02Z notin $ i*) -Set Implicit Arguments. +(** This module defines type constructors for types in [Type] + ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *) -(** This module defines quantification on the world [Type] - ([Logic.v] was defining it on the world [Set]) *) +Set Implicit Arguments. Require Import Datatypes. Require Export Logic. +(** Negation of a type in [Type] *) + Definition notT (A:Type) := A -> False. +(** Conjunction of types in [Type] *) + +Inductive prodT (A B:Type) : Type := + pairT : A -> B -> prodT A B. + +Section prodT_proj. + + Variables A B : Type. + + Definition fstT (H:prodT A B) := match H with + | pairT x _ => x + end. + Definition sndT (H:prodT A B) := match H with + | pairT _ y => y + end. + +End prodT_proj. + +Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) + (x:A) (y:B) : C := f (pairT x y). + +Definition prodT_curry (A B C:Type) (f:A -> B -> C) + (p:prodT A B) : C := match p with + | pairT x y => f x y + end. + +(** Properties of [identity] *) + Section identity_is_a_congruence. Variables A B : Type. @@ -62,28 +92,4 @@ Definition identity_rect_r : intros A x P H y H0; case sym_id with (1 := H0); trivial. Defined. -Inductive prodT (A B:Type) : Type := - pairT : A -> B -> prodT A B. - -Section prodT_proj. - - Variables A B : Type. - - Definition fstT (H:prodT A B) := match H with - | pairT x _ => x - end. - Definition sndT (H:prodT A B) := match H with - | pairT _ y => y - end. - -End prodT_proj. - -Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) - (x:A) (y:B) : C := f (pairT x y). - -Definition prodT_curry (A B C:Type) (f:A -> B -> C) - (p:prodT A B) : C := match p with - | pairT x y => f x y - end. - Hint Immediate sym_id sym_not_id: core v62. |