diff options
| -rw-r--r-- | theories/Init/PeanoSyntax.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v index adb917b765..de3bac0d8e 100644 --- a/theories/Init/PeanoSyntax.v +++ b/theories/Init/PeanoSyntax.v @@ -21,20 +21,21 @@ Delimits Scope nat_scope with N. (* For parsing/printing based on scopes *) Module nat_scope. -Infix LEFTA 4 "+" plus : nat_scope. -Infix LEFTA 3 "*" mult : nat_scope. -Infix 5 "<=" le : nat_scope. -Infix 5 "<" lt : nat_scope. -Infix 5 ">=" ge : nat_scope. -(* Infix 5 ">" gt : nat_scope. (* Conflicts with "<..>Cases ... " *) *) +Infix "+" plus (at level 4) : nat_scope. +Infix "*" mult (at level 3): nat_scope. +Infix "<=" le (at level 5, no associativity) : nat_scope. +Infix "<" lt (at level 5, no associativity) : nat_scope. +Infix ">=" ge (at level 5, no associativity) : nat_scope. +Infix ">" gt (at level 5, no associativity) : nat_scope. (* Warning: this hides sum and prod and breaks sumor symbolic notation *) Open Scope nat_scope. +(* Syntax constr level 0: S' [ (S $p) ] -> [$p:"nat_printer_S":9] | O' [ O ] -> [ _:"nat_printer_O" ] . - +*) End nat_scope. |