From c4bc84f02c7d22402824514d70c6d5e66f511bfc Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 9 Jan 2004 14:45:13 +0000 Subject: Commentaires en v8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5189 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Init/Logic.v | 11 +++++------ 1 file 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 -- cgit v1.2.3