diff options
Diffstat (limited to 'theories/Init/SpecifSyntax.v')
| -rw-r--r-- | theories/Init/SpecifSyntax.v | 55 |
1 files changed, 32 insertions, 23 deletions
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index 9d868cb54..b8bb1dec6 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -11,12 +11,34 @@ Require DatatypesSyntax. Require Specif. +(** Extra factorization of parsing rules *) + +(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *) + +Notation "B + { x : A | P }" := B + (sig A [x:A]P) + (at level 4, left associativity, only parsing) + V8only (at level 40, x at level 80, left associativity, only parsing). + +Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q) + (at level 4, left associativity, only parsing) + V8only (at level 40, x at level 80, left associativity, only parsing). + +Notation "B + { x : A & P }" := B + (sigS A [x:A]P) + (at level 4, left associativity, only parsing) + V8only (at level 40, x at level 80, left associativity, only parsing). + +Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q) + (at level 4, left associativity, only parsing) + V8only (at level 40, x at level 80, left associativity, only parsing). + (** Symbolic notations for things in [Specif.v] *) (* At level 1 to factor with {x:A|P} etc *) -Notation "{ A } + { B }" := (sumbool A B) (at level 1). +Notation "{ A } + { B }" := (sumbool A B) (at level 1) + V8only (at level 10, A at level 80). -Notation "A + { B }" := (sumor A B) (at level 4, left associativity). +Notation "A + { B }" := (sumor A B) (at level 4, left associativity) + V8only (at level 40, B at level 80, left associativity). Notation ProjS1 := (projS1 ? ?). Notation ProjS2 := (projS2 ? ?). @@ -27,28 +49,15 @@ Notation Value := (value ?). Arguments Scope sig [type_scope type_scope]. Arguments Scope sig2 [type_scope type_scope type_scope]. -Notation "{ x : A | P }" := (sig A [x:A]P) (at level 1). -Notation "{ x : A | P & Q }" := (sig2 A [x:A]P [x:A]Q) (at level 1). +Notation "{ x : A | P }" := (sig A [x:A]P) (at level 1) + V8only (at level 10, x at level 80). +Notation "{ x : A | P & Q }" := (sig2 A [x:A]P [x:A]Q) (at level 1) + V8only (at level 10, x at level 80). Arguments Scope sigS [type_scope type_scope]. Arguments Scope sigS2 [type_scope type_scope type_scope]. -Notation "{ x : A & P }" := (sigS A [x:A]P) (at level 1). -Notation "{ x : A & P & Q }" := (sigS2 A [x:A]P [x:A]Q) (at level 1). - -(** Extra factorization of parsing rules *) - -(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *) - -Notation "B + { x : A | P }" := B + ({x:A | P}) - (at level 4, left associativity, only parsing). - -Notation "B + { x : A | P & Q }" := B + ({x:A | P & Q}) - (at level 4, left associativity, only parsing). - -Notation "B + { x : A & P }" := B + ({x:A & P}) - (at level 4, left associativity, only parsing). - -Notation "B + { x : A & P & Q }" := B + ({x:A & P & Q}) - (at level 4, left associativity, only parsing). - +Notation "{ x : A & P }" := (sigS A [x:A]P) (at level 1) + V8only (at level 10, x at level 80). +Notation "{ x : A & P & Q }" := (sigS2 A [x:A]P [x:A]Q) (at level 1) + V8only (at level 10, x at level 80). |