chore: update stage0

stage0/src/Lean/Parser/Parser.lean

@@ -1082,17 +1082,15 @@ let asciiSym := asciiSym.trim;
 { info := unicodeSymbolInfo sym asciiSym,
   fn   := unicodeSymbolFn sym asciiSym }
 
-/- Succeeds if prec <= upper -/
-def checkPrecFn (upper : Nat) (errorMsg : String) : ParserFn :=
+/- Succeeds if `c.prec <= prec` -/
+def checkPrecFn (prec : Nat) : ParserFn :=
 fun c s =>
-  if c.prec <= upper then s
-  else s.mkUnexpectedError errorMsg
+  if c.prec <= prec then s
+  else s.mkUnexpectedError "unexpected token at this precedence level; consider parenthesizing the term"
 
-private def precErrorMsg := "unexpected token at this precedence level; consider parenthesizing the term"
-
-@[inline] def checkPrec (upper : Nat) (errorMsg : String := precErrorMsg) : Parser :=
+@[inline] def checkPrec (prec : Nat) : Parser :=
 { info := epsilonInfo,
-  fn   := checkPrecFn upper errorMsg }
+  fn   := checkPrecFn prec }
 
 /- Version of `leadingNode` which uses `checkPrec` -/
 @[inline] def leadingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser :=

stage0/src/Lean/Parser/Term.lean

@@ -91,7 +91,7 @@ def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >>
 def implicitBinder (requireType := false) := parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
 def instBinder := parser! "[" >> optIdent >> termParser >> "]"
 def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder
-@[builtinTermParser] def depArrow := parser! [appPrec] bracketedBinder true >> checkPrec 25 "expected parentheses around dependent arrow" >> unicodeSymbol " → " " -> " >> termParser
+@[builtinTermParser] def depArrow := parser! [appPrec] bracketedBinder true >> checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser
 def simpleBinder := parser! many1 binderIdent
 @[builtinTermParser] def «forall» := parser! [leadPrec] unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser
 

stage0/src/frontends/lean/builtin_exprs.cpp

@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
+#include "frontends/lean/prenum.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/match_expr.h"
 #include "frontends/lean/brackets.h"
@@ -784,22 +785,16 @@ expr mk_annotation_with_pos(parser &, name const & a, expr const & e, pos_info c
 }
 
 static expr parse_parser(parser & p, bool leading, pos_info const & pos) {
-    name kind     = get_curr_declaration_name();
-    optional<expr> prec;
+    name kind = get_curr_declaration_name();
+    expr prec = save_pos(mk_prenum(mpz(get_max_prec())), pos);
     if (p.curr_is_token(get_lbracket_tk())) {
         p.next();
         prec = p.parse_expr();
         p.check_token_next(get_rbracket_tk(), "`]` expected");
     }
     expr e = p.parse_expr();
-    expr r;
-    if (prec) {
-        name n = leading ? get_lean_parser_leading_node_prec_name() : get_lean_parser_trailing_node_prec_name();
-        r = mk_app(mk_constant(n), quote(kind), *prec, e);
-    } else {
-        name n = leading ? get_lean_parser_leading_node_name() : get_lean_parser_trailing_node_name();
-        r = mk_app(mk_constant(n), quote(kind), e);
-    }
+    name n = leading ? get_lean_parser_leading_node_prec_name() : get_lean_parser_trailing_node_prec_name();
+    expr r = mk_app(mk_constant(n), quote(kind), prec, e);
     if (leading && kind.is_string()) {
         r = mk_app(mk_constant({"Lean", "Parser", "withAntiquot"}),
                    mk_app(mk_constant({"Lean", "Parser", "mkAntiquot"}),