diff options
| -rw-r--r-- | CHANGES | 9 | ||||
| -rwxr-xr-x | theories/Init/Logic.v | 9 |
2 files changed, 14 insertions, 4 deletions
@@ -4,7 +4,7 @@ Changes from V8.0 Syntax - No more support for version 7 syntax and for translation to version 8 syntax. -- Support for primitive interpretation of string litterals +- Support for primitive interpretation of string literals - Extended support for Unicode ranges (Unicode doc TODO) Environment variables @@ -84,9 +84,10 @@ Modules Notations -- "format" option aware of recursive notations -- added insertion of spaces by default in recursive notations w/o separators -- no more automatic printing box in case of user-provided printing "format" +- "format" option aware of recursive notations. +- added insertion of spaces by default in recursive notations w/o separators. +- no more automatic printing box in case of user-provided printing "format". +- new notation "exists! x:A, P" for unique existence. Library diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index cefbb989de..f50e796827 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -141,6 +141,15 @@ 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 *) |