diff options
| -rwxr-xr-x | theories/Init/Logic.v | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index f50e796827..8a11a43bad 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -141,16 +141,6 @@ Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q)) format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'") : type_scope. -Notation "'exists' ! x , P" := - (exists x', (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'') - (at level 200, x ident, right associativity, - format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope. -Notation "'exists' ! x : A , P" := - (exists x' : A, (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'') - (at level 200, x ident, right associativity, - format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope. - - (** Derived rules for universal quantification *) Section universal_quantification. @@ -289,3 +279,14 @@ Proof. Qed. Hint Immediate sym_eq sym_not_eq: core v62. + +(** Other notations *) + +Notation "'exists' ! x , P" := + (exists x', (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'') + (at level 200, x ident, right associativity, + format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope. +Notation "'exists' ! x : A , P" := + (exists x' : A, (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'') + (at level 200, x ident, right associativity, + format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope. |