diff options
Diffstat (limited to 'theories/Init/LogicSyntax.v')
| -rw-r--r-- | theories/Init/LogicSyntax.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index 483221be2b..a16583dd40 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -8,16 +8,18 @@ (*i $Id$ i*) +Require Export Notations. Require Export Logic. (** Symbolic notations for things in [Logic.v] *) +(* V7only[ Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1). ]. Notation "~ x" := (not x) (at level 5, right associativity) V8only (at level 55, right associativity). -Notation "x = y :> T" := (!eq T x y) (at level 5, y at next level, no associativity). +Notation "x = y :> T" := (!eq T x y). Notation "x = y" := (eq ? x y) (at level 5, no associativity). Notation "x <> y :> T" := (not (!eq T x y)) (at level 5, y at next level, no associativity). Notation "x <> y" := (not (eq ? x y)) (at level 5, no associativity). @@ -29,6 +31,7 @@ Infix RIGHTA 8 "<->" iff. Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3) (at level 1, c1, c2, c3 at level 8) V8only (at level 200). +*) (* Order is important to give printing priority to fully typed ALL and EX *) @@ -52,10 +55,12 @@ Notation "'EX' x : t | p & q" := (ex2 t [x:t]p [x:t]q) (at level 10, p, q at level 8) V8only "'EX2' x : t | p & q" (at level 200, x at level 80). +V7only[ (** Parsing only of things in [Logic.v] *) -V7only[ Notation "< A > 'All' ( P )" := (all A P) (A annot, at level 1, only parsing). Notation "< A > x = y" := (eq A x y) (A annot, at level 1, x at level 0, only parsing). +Notation "< A > x <> y" := ~(eq A x y) + (A annot, at level 1, x at level 0, only parsing). ]. |