feat: add builtin prec/prio parsers

src/Init/Meta.lean

@@ -635,7 +635,7 @@ instance Option.hasQuote {α : Type} [Quote α] : Quote (Option α) where
 
 /- Evaluator for `prec` DSL -/
 partial def evalPrec : Syntax → MacroM Nat
-  | `(prec| $num:numLit) => return num.isNatLit?.getD 0
+--  | `(prec| $num:numLit) => return num.isNatLit?.getD 0
   | `(prec| $a + $b) => return (← evalPrec a) + (← evalPrec b)
   | `(prec| $a - $b) => return (← evalPrec a) - (← evalPrec b)
   | prec => Macro.withIncRecDepth prec do

src/Init/Notation.lean

@@ -12,14 +12,13 @@ import Init.Prelude
 
 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 "max"  : prec => `(1024)
+-- macro "lead" : prec => `(1023)
 macro "(" p:prec ")" : prec => p
 
 -- Basic notation for defining parsers

src/Lean/Parser/Syntax.lean

@@ -37,6 +37,11 @@ def «precedence» := parser! ":" >> precedenceLit
 def optPrecedence := optional (atomic «precedence»)
 
 namespace Syntax
+@[builtinPrecParser] def numPrec := checkPrec maxPrec >> numLit
+
+@[builtinPrioParser] def numPrio  := checkPrec maxPrec >> numLit
+@[builtinPrioParser] def highPrio := parser!:maxPrec nonReservedSymbol "high" true
+
 @[builtinSyntaxParser] def paren           := parser! "(" >> many1 syntaxParser >> ")"
 @[builtinSyntaxParser] def cat             := parser! ident >> optPrecedence
 @[builtinSyntaxParser] def unary           := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")"