chore: update stage0

stage0/src/Lean/Elab/Tactic/Induction.lean

@@ -217,7 +217,7 @@ end ElimApp
   Recall that
   ```
   generalizingVars := optional (" generalizing " >> many1 ident)
-  «induction»  := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts
+  «induction»  := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> optional inductionAlts
   ```
   `stx` is syntax for `induction`. -/
 private def getGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :=
@@ -239,22 +239,26 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat :
       Meta.throwTacticEx `induction mvarId "major premise depends on variable being generalized"
     pure (fvarIds.size, [mvarId'])
 
-private def getAlts (withAlts : Syntax) : Array Syntax :=
-  withAlts[1].getSepArgs
+private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
+  inductionAlts[1].getSepArgs
+
+private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
+  if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]
 
 /-
   We may have at most one `| _ => ...` (wildcard alternative), and it must not set variable names.
   The idea is to make sure users do not write unstructured tactics. -/
-private def checkAlts (withAlts : Syntax) : TacticM Unit := do
-  let mut found := false
-  for alt in getAlts withAlts do
-    let n := getAltName alt
-    if n == `_ then
-      unless (getAltVarNames alt).isEmpty do
-        throwErrorAt! alt "wildcard alternative must not specify variable names"
-      if found then
-        throwErrorAt! alt "more than one wildcard alternative '| _ => ...' used"
-      found := true
+private def checkAltsOfOptInductionAlts (optInductionAlts : Syntax) : TacticM Unit :=
+  unless optInductionAlts.isNone do
+    let mut found := false
+    for alt in getAltsOfInductionAlts optInductionAlts[0] do
+      let n := getAltName alt
+      if n == `_ then
+        unless (getAltVarNames alt).isEmpty do
+          throwErrorAt! alt "wildcard alternative must not specify variable names"
+        if found then
+          throwErrorAt! alt "more than one wildcard alternative '| _ => ...' used"
+        found := true
 
 /-
   Given alts of the form
@@ -314,17 +318,17 @@ def getRecFromUsing (major : Expr) (baseRecName : Name) : TacticM Meta.RecursorI
       throwError! "invalid recursor name '{baseRecName}'"
 
 /- Create `RecInfo` assuming builtin recursor -/
-private def getRecInfoDefault (major : Expr) (withAlts : Syntax) (allowMissingAlts : Bool) : TacticM (RecInfo × Array Name) := do
+private def getRecInfoDefault (major : Expr) (optInductionAlts : Syntax) (allowMissingAlts : Bool) : TacticM (RecInfo × Array Name) := do
   let indVal ← getInductiveValFromMajor major
   let recName := mkRecName indVal.name
-  if withAlts.isNone then
+  if optInductionAlts.isNone then
     pure ({ recName := recName }, #[])
   else
     let ctorNames   := indVal.ctors
-    let alts        := getAlts withAlts
+    let alts        := getAltsOfInductionAlts optInductionAlts[0]
     checkAltCtorNames alts ctorNames
     let mut altsNew := #[]
-    -- This code can be simplified if we decide to keep `checkAlts`
+    -- This code can be simplified if we decide to keep `checkAltsOfOptInductionAlts`
     let mut remainingAlts := alts
     let mut prevAnonymousAlt? := none
     for ctorName in ctorNames do
@@ -354,27 +358,28 @@ private def getRecInfoDefault (major : Expr) (withAlts : Syntax) (allowMissingAl
 /-
   Recall that
   ```
-  inductionAlt  : Parser :=
-    nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> (hole <|> syntheticHole <|> tacticParser)
-  inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")
-  withAlts : Parser := optional (" with " >> inductionAlts)
+  altRHS := Term.hole <|> Term.syntheticHole <|> tacticSeq
+  inductionAlt  : Parser := parser! ident' >> many ident' >> darrow >> altRHS
+  inductionAlts : Parser := parser! withPosition ("| " >> sepBy1 inductionAlt (checkColGe "alternatives must be indented" >> "|"))
   usingRec : Parser := optional (" using " >> ident)
+  generalizingVars := optional (" generalizing " >> many1 ident)
+  induction := parser! nonReservedSymbol "induction " >> sepBy1 termParser ", " >> usingRec >> generalizingVars >> optional inductionAlts
   ``` -/
 private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRef stx $ withMainMVarContext do
   let usingRecStx := stx[2]
-  let withAlts    := stx[4]
-  checkAlts withAlts
+  let optInductionAlts := stx[4]
+  checkAltsOfOptInductionAlts optInductionAlts
   if usingRecStx.isNone then
-    let (rinfo, _) ← getRecInfoDefault major withAlts false
+    let (rinfo, _) ← getRecInfoDefault major optInductionAlts false
     pure rinfo
   else
     let baseRecName := usingRecStx.getIdAt 1 $.eraseMacroScopes
     let recInfo ← getRecFromUsing major baseRecName
     let recName := recInfo.recursorName
-    if withAlts.isNone then
+    if optInductionAlts.isNone then
       pure { recName := recName }
     else
-      let alts := getAlts withAlts
+      let alts := getAltsOfInductionAlts optInductionAlts[0]
       let paramNames ← liftMetaMAtMain fun _ => getParamNames recInfo.recursorName
       let mut remainingAlts     := alts
       let mut prevAnonymousAlt? := none
@@ -451,8 +456,8 @@ private def generalizeTerm (term : Expr) : TacticM Expr := do
       let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i]
       let targetFVarIds := targets.map (·.fvarId!)
       ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetFVarIds
-      let withAlts := stx[4]
-      ElimApp.evalAlts elimInfo result.alts (getAlts withAlts) (numGeneralized := n) (toClear := targetFVarIds)
+      let optInductionAlts := stx[4]
+      ElimApp.evalAlts elimInfo result.alts (getAltsOfOptInductionAlts optInductionAlts) (numGeneralized := n) (toClear := targetFVarIds)
 
 private partial def checkCasesResult (casesResult : Array Meta.CasesSubgoal) (ctorNames : Array Name) (alts : Array Syntax) : TacticM Unit := do
   let rec loop (i j : Nat) : TacticM Unit :=
@@ -513,9 +518,9 @@ def elabTargets (targets : Array Syntax) : TacticM (Array Expr) :=
 builtin_initialize registerTraceClass `Elab.cases
 
 /- Default `cases` tactic that uses `casesOn` eliminator -/
-def evalCasesOn (target : Expr) (withAlts : Syntax) : TacticM Unit := do
+def evalCasesOn (target : Expr) (optInductionAlts : Syntax) : TacticM Unit := do
   let (mvarId, _) ← getMainGoal
-  let (recInfo, ctorNames) ← getRecInfoDefault target withAlts true
+  let (recInfo, ctorNames) ← getRecInfoDefault target optInductionAlts (allowMissingAlts := true)
   let altVars := recInfo.alts.map fun alt => (getAltVarNames alt).toList
   let result ← Meta.cases mvarId target.fvarId! altVars
   trace[Elab.cases]! "recInfo.alts.size: #{recInfo.alts.size} {recInfo.alts.map getAltVarNames}"
@@ -525,7 +530,7 @@ def evalCasesOn (target : Expr) (withAlts : Syntax) : TacticM Unit := do
   let alts := recInfo.alts.filter fun stx => !stx.isMissing
   processResult alts result
 
-def evalCasesUsing (elimId : Syntax) (targetRef : Syntax) (targets : Array Expr) (withAlts : Syntax) : TacticM Unit := do
+def evalCasesUsing (elimId : Syntax) (targetRef : Syntax) (targets : Array Expr) (optInductionAlts : Syntax) : TacticM Unit := do
   let elimName := elimId.getId
   let elimInfo ← withRef elimId do getElimInfo elimName
   let (mvarId, _) ← getMainGoal
@@ -540,18 +545,18 @@ def evalCasesUsing (elimId : Syntax) (targetRef : Syntax) (targets : Array Expr)
     withMVarContext mvarId do
       ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetsNew
       assignExprMVar mvarId result.elimApp
-      ElimApp.evalAlts elimInfo result.alts (getAlts withAlts) (numEqs := targets.size)
+      ElimApp.evalAlts elimInfo result.alts (getAltsOfOptInductionAlts optInductionAlts) (numEqs := targets.size)
 
 @[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx => focusAux do
-  -- parser! nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> withAlts
+  -- parser! nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> optInductionAlts
   let targets ← elabTargets stx[1].getSepArgs
-  let withAlts := stx[3]
-  checkAlts withAlts
+  let optInductionAlts := stx[3]
+  checkAltsOfOptInductionAlts optInductionAlts
   if stx[2].isNone then
     unless targets.size == 1 do
       throwErrorAt stx[1] "multiple targets are only supported when a user-defined eliminator is provided with 'using'"
-    evalCasesOn targets[0] withAlts
+    evalCasesOn targets[0] optInductionAlts
   else
-    evalCasesUsing stx[2][1] (targetRef := stx[1]) targets withAlts
+    evalCasesUsing stx[2][1] (targetRef := stx[1]) targets optInductionAlts
 
 end Lean.Elab.Tactic

stage0/src/Lean/Parser/Syntax.lean

@@ -30,7 +30,7 @@ namespace Syntax
 @[builtinSyntaxParser] def unary           := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")"
 @[builtinSyntaxParser] def binary          := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ", " >> many1 syntaxParser >> ")"
 @[builtinSyntaxParser] def atom            := parser! strLit
-@[builtinSyntaxParser] def nonReserved     := parser! "!" >> strLit
+@[builtinSyntaxParser] def nonReserved     := parser! "&" >> strLit
 
 end Syntax
 

stage0/src/Lean/Parser/Tactic.lean

@@ -48,14 +48,13 @@ def rwRuleSeq := parser! "[" >> sepBy1 rwRule ", " true >> "]"
 @[builtinTacticParser 1] def «rewriteSeq» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRuleSeq >> optional location
 
 def altRHS := Term.hole <|> Term.syntheticHole <|> tacticSeq
-def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> altRHS
-def inductionAlts : Parser := withPosition $ "| " >> sepBy1 inductionAlt (checkColGe "alternatives must be indented" >> "|")
-def withAlts : Parser := optional inductionAlts
+def inductionAlt  : Parser := parser! ident' >> many ident' >> darrow >> altRHS
+def inductionAlts : Parser := parser! withPosition ("| " >> sepBy1 inductionAlt (checkColGe "alternatives must be indented" >> "|"))
 def usingRec : Parser := optional (" using " >> ident)
 def generalizingVars := optional (" generalizing " >> many1 ident)
-@[builtinTacticParser] def «induction»  := parser! nonReservedSymbol "induction " >> sepBy1 termParser ", " >> usingRec >> generalizingVars >> withAlts
-def majorPremise := parser! optional (atomic (ident >> " : ")) >> termParser
-@[builtinTacticParser] def «cases»      := parser! nonReservedSymbol "cases " >> sepBy1 majorPremise ", " >> usingRec >> withAlts
+@[builtinTacticParser] def «induction»  := parser! nonReservedSymbol "induction " >> sepBy1 termParser ", " >> usingRec >> generalizingVars >> optional inductionAlts
+def casesTarget := parser! optional (atomic (ident >> " : ")) >> termParser
+@[builtinTacticParser] def «cases»      := parser! nonReservedSymbol "cases " >> sepBy1 casesTarget ", " >> usingRec >> optional inductionAlts
 
 def matchAlt  : Parser := parser! sepBy1 termParser ", " >> darrow >> altRHS
 def matchAlts : Parser := parser! withPosition $ "| " >> sepBy1 matchAlt (checkColGe "alternatives must be indented" >> "| ")

stage0/stdlib/Lean/Parser/Syntax.c

@@ -130,7 +130,6 @@ lean_object* l_Lean_Parser_Command_mixfix_formatter___closed__7;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_elab__rules(lean_object*);
 lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_macroHead;
-extern lean_object* l_Lean_Parser_Term_bnot___closed__1;
 lean_object* l_Lean_Parser_Command_elabTail___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Syntax_paren___closed__4;
 lean_object* l_Lean_Parser_Command_elab_parenthesizer___closed__10;
@@ -310,7 +309,6 @@ lean_object* l_Lean_Parser_Syntax_nonReserved___closed__6;
 lean_object* l_Lean_Parser_precedence___elambda__1___closed__4;
 lean_object* l_Lean_Parser_optPrecedence;
 lean_object* l_Lean_Parser_Command_elab__rules___closed__10;
-extern lean_object* l_Lean_Parser_Term_bnot___elambda__1___closed__6;
 lean_object* l_Lean_Parser_optPrecedence_formatter___closed__2;
 lean_object* l_Lean_Parser_Command_elab___closed__5;
 extern lean_object* l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
@@ -672,6 +670,7 @@ lean_object* l_Lean_Parser_Term_stx_quot___closed__1;
 lean_object* l_Lean_Parser_Command_parserKindPrio___closed__1;
 lean_object* l_Lean_Parser_Command_syntaxCat_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Syntax_nonReserved_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Syntax_nonReserved___closed__7;
 lean_object* l_Lean_Parser_Command_macroTailTactic;
 lean_object* l_Lean_Parser_Command_syntaxAbbrev_parenthesizer___closed__5;
 lean_object* l_Lean_Parser_Command_syntaxAbbrev___closed__6;
@@ -724,6 +723,7 @@ lean_object* l_Lean_Parser_Command_macroTailCommand_formatter___closed__3;
 lean_object* l_Lean_Parser_Command_macro__rules_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Command_syntax_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Command_infix___closed__6;
+lean_object* l_Lean_Parser_Syntax_nonReserved_formatter___closed__4;
 lean_object* l_Lean_Parser_Command_infixr___closed__3;
 lean_object* l_Lean_Parser_Command_elab_parenthesizer___closed__8;
 lean_object* l_Lean_Parser_Command_identPrec___elambda__1___closed__1;
@@ -974,6 +974,7 @@ lean_object* l_Lean_Parser_Command_notationItem___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_infixl_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_notation_parenthesizer___closed__5;
 lean_object* l___regBuiltin_Lean_Parser_Syntax_paren_formatter___closed__1;
+lean_object* l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__10;
 lean_object* l_Lean_Parser_Syntax_atom___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_infix___elambda__1___closed__2;
@@ -1118,12 +1119,12 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_optional_parenthesizer(lean_obje
 lean_object* l_Lean_Parser_nodeFn(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_optKind_formatter___closed__2;
 lean_object* l_Lean_Parser_Syntax_binary_parenthesizer___closed__5;
-extern lean_object* l_Lean_Parser_Term_bnot_formatter___closed__2;
 lean_object* l_Lean_Parser_Command_macroTailTactic___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__8;
 lean_object* l_Lean_Parser_optionalFn(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_mixfixKind___closed__3;
 lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__1;
+lean_object* l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Command_elab___elambda__1___closed__12;
 lean_object* l_Lean_Parser_Command_syntax_formatter___closed__7;
 lean_object* l_Lean_Parser_Command_optKind___closed__1;
@@ -1174,6 +1175,7 @@ lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_Parser_Term_stx_quot___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_elab__rules___elambda__1___closed__5;
 lean_object* l___regBuiltin_Lean_Parser_Syntax_unary_formatter___closed__1;
+lean_object* l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Command_macro_parenthesizer___closed__3;
 lean_object* l_Lean_Parser_Command_macro_formatter___closed__10;
 lean_object* l_Lean_Parser_Term_stx_quot___elambda__1___closed__2;
@@ -4100,8 +4102,35 @@ return x_4;
 static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__5() {
 _start:
 {
+lean_object* x_1; 
+x_1 = lean_mk_string("&");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__6() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__5;
+x_2 = l_String_trim(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__7() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__6;
+x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___boxed), 3, 1);
+lean_closure_set(x_2, 0, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__8() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_bnot___elambda__1___closed__6;
+x_1 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__7;
 x_2 = l_Lean_Parser_strLit___closed__2;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
@@ -4109,24 +4138,24 @@ lean_closure_set(x_3, 1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__6() {
+static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__2;
-x_2 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__5;
+x_2 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__8;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__7() {
+static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__10() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__8;
-x_2 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__6;
+x_2 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__9;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
@@ -4140,7 +4169,7 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object*
 x_3 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__4;
 x_4 = lean_ctor_get(x_3, 1);
 lean_inc(x_4);
-x_5 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__7;
+x_5 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__10;
 x_6 = 1;
 x_7 = l_Lean_Parser_orelseFnCore(x_4, x_5, x_6, x_1, x_2);
 return x_7;
@@ -4149,48 +4178,57 @@ return x_7;
 static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___closed__1() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_strLit;
-x_2 = lean_ctor_get(x_1, 0);
-lean_inc(x_2);
-x_3 = l_Lean_Parser_Term_bnot___closed__1;
-x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
-return x_4;
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__6;
+x_2 = l_Lean_Parser_symbolInfo(x_1);
+return x_2;
 }
 }
 static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___closed__2() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__2;
-x_2 = l_Lean_Parser_Syntax_nonReserved___closed__1;
-x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_strLit;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Syntax_nonReserved___closed__1;
+x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
+return x_4;
 }
 }
 static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
+x_1 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__2;
 x_2 = l_Lean_Parser_Syntax_nonReserved___closed__2;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
 static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___closed__4() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_epsilonInfo;
+x_2 = l_Lean_Parser_Syntax_nonReserved___closed__3;
+x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___closed__5() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__4;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Syntax_nonReserved___closed__3;
+x_3 = l_Lean_Parser_Syntax_nonReserved___closed__4;
 x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___closed__5() {
+static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___closed__6() {
 _start:
 {
 lean_object* x_1; 
@@ -4198,12 +4236,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_nonReserved___elambda__1),
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___closed__6() {
+static lean_object* _init_l_Lean_Parser_Syntax_nonReserved___closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Syntax_nonReserved___closed__4;
-x_2 = l_Lean_Parser_Syntax_nonReserved___closed__5;
+x_1 = l_Lean_Parser_Syntax_nonReserved___closed__5;
+x_2 = l_Lean_Parser_Syntax_nonReserved___closed__6;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -4214,7 +4252,7 @@ static lean_object* _init_l_Lean_Parser_Syntax_nonReserved() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Syntax_nonReserved___closed__6;
+x_1 = l_Lean_Parser_Syntax_nonReserved___closed__7;
 return x_1;
 }
 }
@@ -4249,8 +4287,18 @@ return x_5;
 static lean_object* _init_l_Lean_Parser_Syntax_nonReserved_formatter___closed__2() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__5;
+x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter___boxed), 6, 1);
+lean_closure_set(x_2, 0, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Parser_Syntax_nonReserved_formatter___closed__3() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_bnot_formatter___closed__2;
+x_1 = l_Lean_Parser_Syntax_nonReserved_formatter___closed__2;
 x_2 = l_Lean_Parser_Term_str_formatter___closed__1;
 x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
 lean_closure_set(x_3, 0, x_1);
@@ -4258,13 +4306,13 @@ lean_closure_set(x_3, 1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Parser_Syntax_nonReserved_formatter___closed__3() {
+static lean_object* _init_l_Lean_Parser_Syntax_nonReserved_formatter___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__2;
 x_2 = lean_unsigned_to_nat(1024u);
-x_3 = l_Lean_Parser_Syntax_nonReserved_formatter___closed__2;
+x_3 = l_Lean_Parser_Syntax_nonReserved_formatter___closed__3;
 x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
 lean_closure_set(x_4, 0, x_1);
 lean_closure_set(x_4, 1, x_2);
@@ -4277,7 +4325,7 @@ _start:
 {
 lean_object* x_6; lean_object* x_7; lean_object* x_8; 
 x_6 = l_Lean_Parser_Syntax_nonReserved_formatter___closed__1;
-x_7 = l_Lean_Parser_Syntax_nonReserved_formatter___closed__3;
+x_7 = l_Lean_Parser_Syntax_nonReserved_formatter___closed__4;
 x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
 return x_8;
 }
@@ -15274,6 +15322,12 @@ l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__6 = _init_l_Lean_Parser_
 lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__6);
 l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__7 = _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__7();
 lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__7);
+l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__8 = _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__8();
+lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__8);
+l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__9 = _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__9();
+lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__9);
+l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__10 = _init_l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__10();
+lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved___elambda__1___closed__10);
 l_Lean_Parser_Syntax_nonReserved___closed__1 = _init_l_Lean_Parser_Syntax_nonReserved___closed__1();
 lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved___closed__1);
 l_Lean_Parser_Syntax_nonReserved___closed__2 = _init_l_Lean_Parser_Syntax_nonReserved___closed__2();
@@ -15286,6 +15340,8 @@ l_Lean_Parser_Syntax_nonReserved___closed__5 = _init_l_Lean_Parser_Syntax_nonRes
 lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved___closed__5);
 l_Lean_Parser_Syntax_nonReserved___closed__6 = _init_l_Lean_Parser_Syntax_nonReserved___closed__6();
 lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved___closed__6);
+l_Lean_Parser_Syntax_nonReserved___closed__7 = _init_l_Lean_Parser_Syntax_nonReserved___closed__7();
+lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved___closed__7);
 l_Lean_Parser_Syntax_nonReserved = _init_l_Lean_Parser_Syntax_nonReserved();
 lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved);
 res = l___regBuiltinParser_Lean_Parser_Syntax_nonReserved(lean_io_mk_world());
@@ -15297,6 +15353,8 @@ l_Lean_Parser_Syntax_nonReserved_formatter___closed__2 = _init_l_Lean_Parser_Syn
 lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved_formatter___closed__2);
 l_Lean_Parser_Syntax_nonReserved_formatter___closed__3 = _init_l_Lean_Parser_Syntax_nonReserved_formatter___closed__3();
 lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved_formatter___closed__3);
+l_Lean_Parser_Syntax_nonReserved_formatter___closed__4 = _init_l_Lean_Parser_Syntax_nonReserved_formatter___closed__4();
+lean_mark_persistent(l_Lean_Parser_Syntax_nonReserved_formatter___closed__4);
 l___regBuiltin_Lean_Parser_Syntax_nonReserved_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Syntax_nonReserved_formatter___closed__1();
 lean_mark_persistent(l___regBuiltin_Lean_Parser_Syntax_nonReserved_formatter___closed__1);
 res = l___regBuiltin_Lean_Parser_Syntax_nonReserved_formatter(lean_io_mk_world());