diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Logic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index d8a028cfb8..ca7d0073e1 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -240,7 +240,7 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x. Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, right associativity, - format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") + format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") : type_scope. Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q)) @@ -423,7 +423,7 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y. Notation "'exists' ! x .. y , p" := (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) (at level 200, x binder, right associativity, - format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'") + format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'") : type_scope. Lemma unique_existence : forall (A:Type) (P:A->Prop), |