diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 6c32ccb380..dbb1b55a5d 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -9,10 +9,15 @@ prelude import Init.Prelude -- DSL for specifying parser precedences -syntax ident : prec -syntax num : prec -syntax:65 prec " + " prec:66 : prec -syntax:65 prec " - " prec:66 : prec + +namespace Lean.Parser.Syntax + +syntax [numPrec] num : prec +syntax:65 [addPrec] prec " + " prec:66 : prec +syntax:65 [subPrec] prec " - " prec:66 : prec + +end Lean.Parser.Syntax + macro "max" : prec => `(1024) macro "lead" : prec => `(1023) macro "(" p:prec ")" : prec => p