aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-01-09 14:45:13 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-01-09 14:45:13 +0000
commitc4bc84f02c7d22402824514d70c6d5e66f511bfc (patch)
tree8ce4bb0a917bc0a5f2cfb5371f0bf4a01211208b
parenteb2f9b5023f6d42f89ddfb3927fda81d6cb334a1 (diff)
Commentaires en v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5189 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xtheories/Init/Logic.v11
1 files changed, 5 insertions, 6 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 31ce20ad3..65fe059be 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -95,18 +95,17 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
(** First-order quantifiers *)
- (** [(ex A P)], or simply [(EX x | P(x))], expresses the existence of an
+ (** [ex A P], or simply [exists x, P x], expresses the existence of an
[x] of type [A] which satisfies the predicate [P] ([A] is of type
[Set]). This is existential quantification. *)
- (** [(ex2 A P Q)], or simply [(EX x | P(x) & Q(x))], expresses the
+ (** [ex2 A P Q], or simply [exists2 x, P x & Q x], expresses the
existence of an [x] of type [A] which satisfies both the predicates
[P] and [Q] *)
(** Universal quantification (especially first-order one) is normally
- written [(x:A)(P x)]. For duality with existential quantification, the
- construction [(all A P)], or simply [(All P)], is provided as an
- abbreviation of [(x:A)(P x)] *)
+ written [forall x:A, P x]. For duality with existential quantification,
+ the construction [all P] is provided too *)
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
ex_intro : forall x:A, P x -> ex (A:=A) P.
@@ -153,7 +152,7 @@ Section universal_quantification.
(** Equality *)
-(** [(eq A x y)], or simply [x=y], expresses the (Leibniz') equality
+(** [eq A x y], or simply [x=y], expresses the (Leibniz') equality
of [x] and [y]. Both [x] and [y] must belong to the same type [A].
The definition is inductive and states the reflexivity of the equality.
The others properties (symmetry, transitivity, replacement of