diff options
Diffstat (limited to 'theories/Init/Logic_TypeSyntax.v')
| -rw-r--r-- | theories/Init/Logic_TypeSyntax.v | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v index 1de550267..9cebfb7df 100644 --- a/theories/Init/Logic_TypeSyntax.v +++ b/theories/Init/Logic_TypeSyntax.v @@ -12,35 +12,37 @@ Require Logic_Type. (** Symbolic notations for things in [Logic_type.v] *) -Notation "x == y" := (eqT ? x y) (at level 5, no associativity). +Notation "x == y" := (eq ? x y) (at level 5, no associativity, only parsing). Notation "x === y" := (identityT ? x y) (at level 5, no associativity). +Notation "'eqT'" := eq (at level 0). + (* Order is important to give printing priority to fully typed ALL and EX *) -Notation AllT := (allT ?). -Notation "'ALLT' x | p" := (allT ? [x]p) (at level 10, p at level 8) +Notation AllT := (all ?). +Notation "'ALLT' x | p" := (all ? [x]p) (at level 10, p at level 8) V8only (at level 200, x at level 80). -Notation "'ALLT' x : t | p" := (allT t [x:t]p) (at level 10, p at level 8) +Notation "'ALLT' x : t | p" := (all t [x:t]p) (at level 10, p at level 8) V8only (at level 200, x at level 80). -Notation ExT := (exT ?). -Notation "'EXT' x | p" := (exT ? [x]p) (at level 10, p at level 8) +Notation ExT := (ex ?). +Notation "'EXT' x | p" := (ex ? [x]p) (at level 10, p at level 8) V8only (at level 200, x at level 80). -Notation "'EXT' x : t | p" := (exT t [x:t]p) (at level 10, p at level 8) +Notation "'EXT' x : t | p" := (ex t [x:t]p) (at level 10, p at level 8) V8only (at level 200, x at level 80). -Notation ExT2 := (exT2 ?). -Notation "'EXT' x | p & q" := (exT2 ? [x]p [x]q) +Notation ExT2 := (ex2 ?). +Notation "'EXT' x | p & q" := (ex2 ? [x]p [x]q) (at level 10, p, q at level 8) V8only "'EXT2' x | p & q" (at level 200, x at level 80). -Notation "'EXT' x : t | p & q" := (exT2 t [x:t]p [x:t]q) +Notation "'EXT' x : t | p & q" := (ex2 t [x:t]p [x:t]q) (at level 10, p, q at level 8) V8only "'EXT2' x : t | p & q" (at level 200, x at level 80). (** Parsing only of things in [Logic_type.v] *) V7only[ -Notation "< A > x == y" := (eqT A x y) +Notation "< A > x == y" := (eq A x y) (A annot, at level 1, x at level 0, only parsing). Notation "< A > x === y" := (identityT A x y) |