diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-21 08:36:12 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-21 08:36:12 +0000 |
| commit | 327c9115cf88d919d8f6b17904764c4147116604 (patch) | |
| tree | 06c8587bd44f1eb030f56272447b70f9bc5c9507 /theories/Init | |
| parent | 05ac4436c1d689aced1cbfe7a4949db77d8a3fc2 (diff) | |
ajouts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4680 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init')
| -rwxr-xr-x | theories/Init/Datatypes.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 43c301fb3..bbc59da42 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -9,6 +9,7 @@ (*i $Id$ i*) Require Notations. +Require Logic. Set Implicit Arguments. V7only [Unset Implicit Arguments.]. @@ -91,9 +92,26 @@ Notation Snd := (snd ? ?). ]. Hints Resolve pair inl inr : core v62. +Lemma surjective_pairing : (A,B:Set;H:A*B)H=(pair A B (Fst H) (Snd H)). +Proof. +NewDestruct H; Reflexivity. +Qed. + V7only[ (** Parsing only of things in [Datatypes.v] *) Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot). Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot). Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot). ]. + +(** Comparison *) + +Inductive relation : Set := + EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation. + +Definition Op := [r:relation] + Cases r of + EGAL => EGAL + | INFERIEUR => SUPERIEUR + | SUPERIEUR => INFERIEUR + end. |