chore: update stage0

stage0/src/Init/Meta.lean

@@ -648,6 +648,10 @@ partial def evalPrec : Syntax → MacroM Nat
 
 macro "evalPrec! " p:prec:max : term => return quote (← evalPrec p)
 
+def evalOptPrec : Option Syntax → MacroM Nat
+  | some prec => evalPrec prec
+  | none      => return 0
+
 end Lean
 
 namespace Array

stage0/src/Lean/Elab/Syntax.lean

@@ -382,14 +382,12 @@ def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
 
 -- TODO: cleanup after we have support for optional syntax at `match_syntax`
 @[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
-  withAttrKindGlobal stx fun stx =>
+  withAttrKindGlobal stx fun stx => do
     match stx with
     | `(infix $[: $prec]? $[[$prio]]? $op => $f)   => `(infixl $[: $prec]? $[[$prio]]? $op => $f)
     | `(infixr $[: $prec]? $[[$prio]]? $op => $f)  => `(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs $[: $prec]? => $f lhs rhs)
     | `(infixl $[: $prec]? $[[$prio]]? $op => $f)  =>
-       let prec1 : Syntax := match (prec : Option Syntax) with
-         | some prec => quote (prec.toNat+1)
-         | none      => quote 0
+       let prec1 := quote <| (← evalOptPrec prec) + 1
        `(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs:$prec1 => $f lhs rhs)
     | `(prefix $[: $prec]? $[[$prio]]? $op => $f)  => `(notation $[: $prec]? $[[$prio]]? $op:strLit arg $[: $prec]? => $f arg)
     | `(postfix $[: $prec]? $[[$prio]]? $op => $f) => `(notation $[: $prec]? $[[$prio]]? arg $op:strLit => $f arg)

stage0/stdlib/Init/Meta.c

@@ -244,6 +244,7 @@ lean_object* l_Lean_instQuoteBool___closed__6;
 extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__14;
 lean_object* l_Lean_mkFreshId___rarg(lean_object*, lean_object*);
 lean_object* l_String_capitalize(lean_object*);
+lean_object* l_Lean_evalOptPrec_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_NameGenerator_next(lean_object*);
 lean_object* l_Lean_Syntax_setHeadInfo_match__1(lean_object*);
 lean_object* l_Lean_Syntax_decodeCharLit___boxed(lean_object*);
@@ -280,6 +281,7 @@ lean_object* l_Lean_NameGenerator_idx___default;
 lean_object* lean_array_to_list(lean_object*, lean_object*);
 lean_object* l_Lean_mkFreshId(lean_object*);
 lean_object* l_Lean_Macro_throwErrorAt___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_evalOptPrec_match__1(lean_object*);
 lean_object* l_Lean_mkCIdent(lean_object*);
 lean_object* l_Lean_mkOptionalNode_match__1(lean_object*);
 lean_object* l_Lean_Syntax_replaceInfo(lean_object*, lean_object*);
@@ -304,6 +306,7 @@ lean_object* l_Lean_Name_appendIndexAfter_match__1(lean_object*);
 lean_object* l_Lean_termEvalPrec_x21_____closed__3;
 lean_object* l___private_Init_Meta_0__Lean_Syntax_decodeNameLitAux___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_copyTailInfo_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_evalOptPrec(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Meta_0__Lean_quoteOption___rarg___closed__4;
 uint8_t l_Array_isEmpty___rarg(lean_object*);
@@ -10280,6 +10283,61 @@ return x_27;
 }
 }
 }
+lean_object* l_Lean_evalOptPrec_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_2);
+x_4 = lean_box(0);
+x_5 = lean_apply_1(x_3, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_3);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_2, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_Lean_evalOptPrec_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_evalOptPrec_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_evalOptPrec(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_2);
+x_4 = lean_unsigned_to_nat(0u);
+x_5 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_5, 0, x_4);
+lean_ctor_set(x_5, 1, x_3);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = l_Lean_evalPrec(x_6, x_2, x_3);
+return x_7;
+}
+}
+}
 lean_object* l_Array_foldlMUnsafe_fold___at_Array_getSepElems___spec__1___rarg(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
 _start:
 {