chore: update stage0

2020-09-19 17:55:57 -07:00 · 2020-09-19 17:55:57 -07:00 · e52f50b2fb
commit e52f50b2fb
parent fe2d3be821
19 changed files with 3520 additions and 2869 deletions
--- a/stage0/src/Lean/Parser/Basic.lean
+++ b/stage0/src/Lean/Parser/Basic.lean
@ -1306,7 +1306,8 @@ fun c s =>
      else
        invalidLongestMatchParser s

-def longestMatchStep (left? : Option Syntax) (startSize : Nat) (startPos : String.Pos) (p : ParserFn) : ParserFn :=
+def longestMatchStep (left? : Option Syntax) (startSize : Nat) (startPos : String.Pos) (prevPrio : Nat) (prio : Nat) (p : ParserFn)
+    : ParserContext → ParserState → ParserState × Nat :=
 fun c s =>
 let prevErrorMsg  := s.errorMsg;
 let prevStopPos   := s.pos;
@ -1315,41 +1316,41 @@ let s             := s.restore prevSize startPos;
 let s             := runLongestMatchParser left? p c s;
 match prevErrorMsg, s.errorMsg with
 | none, none   => -- both succeeded
-  if s.pos > prevStopPos      then s.replaceLongest startSize
-  else if s.pos < prevStopPos then s.restore prevSize prevStopPos -- keep prev
-  else s
+  if s.pos > prevStopPos || (s.pos == prevStopPos && prio > prevPrio)      then (s.replaceLongest startSize, prio)
+  else if s.pos < prevStopPos || (s.pos == prevStopPos && prio < prevPrio) then (s.restore prevSize prevStopPos, prevPrio) -- keep prev
+  else (s, prio)
 | none, some _ => -- prev succeeded, current failed
-  s.restore prevSize prevStopPos
+  (s.restore prevSize prevStopPos, prevPrio)
 | some oldError, some _ => -- both failed
-  if s.pos > prevStopPos      then s.keepNewError prevSize
-  else if s.pos < prevStopPos then s.keepPrevError prevSize prevStopPos prevErrorMsg
-  else s.mergeErrors prevSize oldError
+  if s.pos > prevStopPos || (s.pos == prevStopPos && prio > prevPrio)      then (s.keepNewError prevSize, prio)
+  else if s.pos < prevStopPos || (s.pos == prevStopPos && prio < prevPrio) then (s.keepPrevError prevSize prevStopPos prevErrorMsg, prevPrio)
+  else (s.mergeErrors prevSize oldError, prio)
 | some _, none => -- prev failed, current succeeded
  let successNode := s.stxStack.back;
  let s           := s.shrinkStack startSize; -- restore stack to initial size to make sure (failure) nodes are removed from the stack
-  s.pushSyntax successNode -- put successNode back on the stack
+  (s.pushSyntax successNode, prio) -- put successNode back on the stack

 def longestMatchMkResult (startSize : Nat) (s : ParserState) : ParserState :=
 if !s.hasError && s.stackSize > startSize + 1 then s.mkNode choiceKind startSize else s

-def longestMatchFnAux (left? : Option Syntax) (startSize : Nat) (startPos : String.Pos) : List Parser → ParserFn
-| []    => fun _ s => longestMatchMkResult startSize s
-| p::ps => fun c s =>
-   let s := longestMatchStep left? startSize startPos p.fn c s;
-   longestMatchFnAux ps c s
+def longestMatchFnAux (left? : Option Syntax) (startSize : Nat) (startPos : String.Pos) : Nat → List (Parser × Nat) → ParserFn
+| prevPrio, []    => fun _ s => longestMatchMkResult startSize s
+| prevPrio, p::ps => fun c s =>
+   let (s, prevPrio) := longestMatchStep left? startSize startPos prevPrio p.2 p.1.fn c s;
+   longestMatchFnAux prevPrio ps c s

-def longestMatchFn (left? : Option Syntax) : List Parser → ParserFn
+def longestMatchFn (left? : Option Syntax) : List (Parser × Nat) → ParserFn
 | []    => fun _ s => s.mkError "longestMatch: empty list"
-| [p]   => runLongestMatchParser left? p.fn
+| [p]   => runLongestMatchParser left? p.1.fn
 | p::ps => fun c s =>
  let startSize := s.stackSize;
  let startPos  := s.pos;
-  let s         := runLongestMatchParser left? p.fn c s;
+  let s         := runLongestMatchParser left? p.1.fn c s;
  if s.hasError then
    let s := s.shrinkStack startSize;
-    longestMatchFnAux left? startSize startPos ps c s
+    longestMatchFnAux left? startSize startPos p.2 ps c s
  else
-    longestMatchFnAux left? startSize startPos ps c s
+    longestMatchFnAux left? startSize startPos p.2 ps c s

 def anyOfFn : List Parser → ParserFn
 | [],    _, s => s.mkError "anyOf: empty list"
@ -1393,10 +1394,10 @@ instance {α : Type} : HasEmptyc (TokenMap α) := ⟨RBMap.empty⟩
 end TokenMap

 structure PrattParsingTables :=
-(leadingTable    : TokenMap Parser := {})
-(leadingParsers  : List Parser := []) -- for supporting parsers we cannot obtain first token
-(trailingTable   : TokenMap TrailingParser := {})
-(trailingParsers : List TrailingParser := []) -- for supporting parsers such as function application
+(leadingTable    : TokenMap (Parser × Nat) := {})
+(leadingParsers  : List (Parser × Nat) := []) -- for supporting parsers we cannot obtain first token
+(trailingTable   : TokenMap (Parser × Nat) := {})
+(trailingParsers : List (Parser × Nat) := []) -- for supporting parsers such as function application

 instance PrattParsingTables.inhabited : Inhabited PrattParsingTables := ⟨{}⟩

@ -1608,7 +1609,7 @@ fun c s =>
@[inline] def leadingParser (kind : Name) (tables : PrattParsingTables) (leadingIdentAsSymbol : Bool) (antiquotParser : ParserFn) : ParserFn :=
 withAntiquotFn antiquotParser (leadingParserAux kind tables leadingIdentAsSymbol)

-def trailingLoopStep (tables : PrattParsingTables) (left : Syntax) (ps : List Parser) : ParserFn :=
+def trailingLoopStep (tables : PrattParsingTables) (left : Syntax) (ps : List (Parser × Nat)) : ParserFn :=
 fun c s => longestMatchFn left (ps ++ tables.trailingParsers) c s

 private def mkTrailingResult (s : ParserState) (iniSz : Nat) : ParserState :=
--- a/stage0/src/Lean/Parser/Extension.lean
+++ b/stage0/src/Lean/Parser/Extension.lean
@ -53,13 +53,13 @@ inductive ParserExtensionOleanEntry
 | token     (val : Token) : ParserExtensionOleanEntry
 | kind      (val : SyntaxNodeKind) : ParserExtensionOleanEntry
 | category  (catName : Name) (leadingIdentAsSymbol : Bool)
-| parser    (catName : Name) (declName : Name) : ParserExtensionOleanEntry
+| parser    (catName : Name) (declName : Name) (prio : Nat) : ParserExtensionOleanEntry

 inductive ParserExtensionEntry
 | token     (val : Token) : ParserExtensionEntry
 | kind      (val : SyntaxNodeKind) : ParserExtensionEntry
 | category  (catName : Name) (leadingIdentAsSymbol : Bool)
-| parser    (catName : Name) (declName : Name) (leading : Bool) (p : Parser) : ParserExtensionEntry
+| parser    (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : ParserExtensionEntry

 structure ParserExtensionState :=
 (tokens      : TokenTable := {})
@ -89,40 +89,40 @@ throw ("unknown parser category '" ++ toString catName ++ "'")
 abbrev getCategory (categories : ParserCategories) (catName : Name) : Option ParserCategory :=
 categories.find? catName

-def addLeadingParser (categories : ParserCategories) (catName : Name) (parserName : Name) (p : Parser) : Except String ParserCategories :=
+def addLeadingParser (categories : ParserCategories) (catName : Name) (parserName : Name) (p : Parser) (prio : Nat) : Except String ParserCategories :=
 match getCategory categories catName with
 | none     =>
  throwUnknownParserCategory catName
 | some cat =>
  let addTokens (tks : List Token) : Except String ParserCategories :=
    let tks    := tks.map $ fun tk => mkNameSimple tk;
-    let tables := tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { tables with leadingTable := tables.leadingTable.insert tk p }) cat.tables;
+    let tables := tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { tables with leadingTable := tables.leadingTable.insert tk (p, prio) }) cat.tables;
    pure $ categories.insert catName { cat with tables := tables };
  match p.info.firstTokens with
  | FirstTokens.tokens tks    => addTokens tks
  | FirstTokens.optTokens tks => addTokens tks
  | _ =>
-    let tables := { cat.tables with leadingParsers := p :: cat.tables.leadingParsers };
+    let tables := { cat.tables with leadingParsers := (p, prio) :: cat.tables.leadingParsers };
    pure $ categories.insert catName { cat with tables := tables }

-private def addTrailingParserAux (tables : PrattParsingTables) (p : TrailingParser) : PrattParsingTables :=
+private def addTrailingParserAux (tables : PrattParsingTables) (p : TrailingParser) (prio : Nat) : PrattParsingTables :=
 let addTokens (tks : List Token) : PrattParsingTables :=
  let tks := tks.map $ fun tk => mkNameSimple tk;
-  tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { tables with trailingTable := tables.trailingTable.insert tk p }) tables;
+  tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { tables with trailingTable := tables.trailingTable.insert tk (p, prio) }) tables;
 match p.info.firstTokens with
 | FirstTokens.tokens tks    => addTokens tks
 | FirstTokens.optTokens tks => addTokens tks
-| _                         => { tables with trailingParsers := p :: tables.trailingParsers }
+| _                         => { tables with trailingParsers := (p, prio) :: tables.trailingParsers }

-def addTrailingParser (categories : ParserCategories) (catName : Name) (p : TrailingParser) : Except String ParserCategories :=
+def addTrailingParser (categories : ParserCategories) (catName : Name) (p : TrailingParser) (prio : Nat) : Except String ParserCategories :=
 match getCategory categories catName with
 | none     => throwUnknownParserCategory catName
-| some cat => pure $ categories.insert catName { cat with tables := addTrailingParserAux cat.tables p }
+| some cat => pure $ categories.insert catName { cat with tables := addTrailingParserAux cat.tables p prio }

-def addParser (categories : ParserCategories) (catName : Name) (declName : Name) (leading : Bool) (p : Parser) : Except String ParserCategories :=
+def addParser (categories : ParserCategories) (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : Except String ParserCategories :=
 match leading, p with
-| true, p  => addLeadingParser categories catName declName p
-| false, p => addTrailingParser categories catName p
+| true, p  => addLeadingParser categories catName declName p prio
+| false, p => addTrailingParser categories catName p prio

 def addParserTokens (tokenTable : TokenTable) (info : ParserInfo) : Except String TokenTable :=
 let newTokens := info.collectTokens [];
@ -134,18 +134,24 @@ match addParserTokens tokenTable info with
 | Except.ok tokenTable => builtinTokenTable.set tokenTable
 | Except.error msg     => throw (IO.userError ("invalid builtin parser '" ++ toString declName ++ "', " ++ msg))

-def addBuiltinParser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) : IO Unit := do
+def addBuiltinParser (catName : Name) (declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : IO Unit := do
 categories ← builtinParserCategoriesRef.get;
-categories ← IO.ofExcept $ addParser categories catName declName leading p;
+categories ← IO.ofExcept $ addParser categories catName declName leading p prio;
 builtinParserCategoriesRef.set categories;
 builtinSyntaxNodeKindSetRef.modify p.info.collectKinds;
 updateBuiltinTokens p.info declName

+def addBuiltinLeadingParserNew (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
+addBuiltinParser catName declName true p prio
+
+def addBuiltinTrailingParserNew (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
+addBuiltinParser catName declName false p prio
+
 def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) : IO Unit :=
-addBuiltinParser catName declName true p
+addBuiltinParser catName declName true p 0

 def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) : IO Unit :=
-addBuiltinParser catName declName false p
+addBuiltinParser catName declName false p 0

 private def ParserExtension.addEntry (s : ParserExtensionState) (e : ParserExtensionEntry) : ParserExtensionState :=
 match e with
@ -160,9 +166,9 @@ match e with
  else { s with
         categories := s.categories.insert catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol },
         newEntries := ParserExtensionOleanEntry.category catName leadingIdentAsSymbol :: s.newEntries }
-| ParserExtensionEntry.parser catName declName leading parser =>
-  match addParser s.categories catName declName leading parser with
-  | Except.ok categories => { s with categories := categories, newEntries := ParserExtensionOleanEntry.parser catName declName :: s.newEntries }
+| ParserExtensionEntry.parser catName declName leading parser prio =>
+  match addParser s.categories catName declName leading parser prio with
+  | Except.ok categories => { s with categories := categories, newEntries := ParserExtensionOleanEntry.parser catName declName prio :: s.newEntries }
  | _ => unreachable!

 unsafe def mkParserOfConstantUnsafe
@ -261,9 +267,9 @@ es.foldlM
       | ParserExtensionOleanEntry.category catName leadingIdentAsSymbol => do
         categories ← IO.ofExcept (addParserCategoryCore s.categories catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol});
         pure { s with categories := categories }
-       | ParserExtensionOleanEntry.parser catName declName => do
+       | ParserExtensionOleanEntry.parser catName declName prio => do
         p ← IO.ofExcept $ mkParserOfConstant env s.categories declName;
-         categories ← IO.ofExcept $ addParser s.categories catName declName p.1 p.2;
+         categories ← IO.ofExcept $ addParser s.categories catName declName p.1 p.2 prio;
         -- discard result env; all environment side effects should already have happened when the parser was declared initially
         _ ← (runParserAttributeHooks catName declName /- builtin -/ false).toIO {} { env := env };
         pure { s with categories := categories })
@ -362,34 +368,42 @@ else if input.atEnd s.pos then
 else
  Except.error ((s.mkError "end of input").toErrorMsg c)

-def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) (declName : Name) : IO Environment :=
+def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) (declName : Name) (prio : Nat) : IO Environment :=
 let name := `_regBuiltinParser ++ declName;
 let type := mkApp (mkConst `IO) (mkConst `Unit);
-let val  := mkAppN (mkConst addFnName) #[toExpr catName, toExpr declName, mkConst declName];
+let val  := mkAppN (mkConst addFnName) #[toExpr catName, toExpr declName, mkConst declName, mkNatLit prio];
 let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
 match env.addAndCompile {} decl with
 -- TODO: pretty print error
 | Except.error _ => throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'"))
 | Except.ok env  => IO.ofExcept (setInitAttr env name)

-def declareLeadingBuiltinParser (env : Environment) (catName : Name) (declName : Name) : IO Environment := -- TODO: use CoreM?
-declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParser catName declName
+def declareLeadingBuiltinParser (env : Environment) (catName : Name) (declName : Name) (prio : Nat) : IO Environment := -- TODO: use CoreM?
+declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParserNew catName declName prio

-def declareTrailingBuiltinParser (env : Environment) (catName : Name) (declName : Name) : IO Environment := -- TODO: use CoreM?
-declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParser catName declName
+def declareTrailingBuiltinParser (env : Environment) (catName : Name) (declName : Name) (prio : Nat) : IO Environment := -- TODO: use CoreM?
+declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParserNew catName declName prio
+
+def getParserPriority (args : Syntax) : Except String Nat :=
+match args.getNumArgs with
+| 0 => pure 0
+| 1 => match (args.getArg 0).isNatLit? with
+  | some prio => pure prio
+  | none => throw "invalid parser attribute, numeral expected"
+| _ => throw "invalid parser attribute, no argument or numeral expected"

 private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
    (declName : Name) (args : Syntax) (persistent : Bool) : CoreM Unit := do
-when args.hasArgs $ throwError ("invalid attribute '" ++ attrName ++ "', unexpected argument");
+prio ← ofExcept (getParserPriority args);
 unless persistent $ throwError ("invalid attribute '" ++ attrName ++ "', must be persistent");
 decl ← getConstInfo declName;
 env ← getEnv;
 match decl.type with
 | Expr.const `Lean.Parser.TrailingParser _ _ => do
-  env ← liftIO $ declareTrailingBuiltinParser env catName declName;
+  env ← liftIO $ declareTrailingBuiltinParser env catName declName prio;
  setEnv env
 | Expr.const `Lean.Parser.Parser _ _ => do
-  env ← liftIO $ declareLeadingBuiltinParser env catName declName;
+  env ← liftIO $ declareLeadingBuiltinParser env catName declName prio;
  setEnv env
 | _ => throwError ("unexpected parser type at '" ++ declName ++ "' (`Parser` or `TrailingParser` expected");
 runParserAttributeHooks catName declName /- builtin -/ true
@ -407,7 +421,7 @@ registerBuiltinAttribute {
 }

 private def ParserAttribute.add (attrName : Name) (catName : Name) (declName : Name) (args : Syntax) (persistent : Bool) : CoreM Unit := do
-when args.hasArgs $ throwError ("invalid attribute '" ++ attrName ++ "', unexpected argument");
+prio ← ofExcept (getParserPriority args);
 env ← getEnv;
 let categories := (parserExtension.getState env).categories;
 match mkParserOfConstant env categories declName with
@ -424,8 +438,8 @@ match mkParserOfConstant env categories declName with
  };
  let kinds := parser.info.collectKinds {};
  kinds.forM fun kind _ => modifyEnv fun env => addSyntaxNodeKind env kind;
-  match addParser categories catName declName leading parser with
-  | Except.ok _     => modifyEnv fun env => parserExtension.addEntry env $ ParserExtensionEntry.parser catName declName leading parser
+  match addParser categories catName declName leading parser prio with
+  | Except.ok _     => modifyEnv fun env => parserExtension.addEntry env $ ParserExtensionEntry.parser catName declName leading parser prio
  | Except.error ex => throwError ex;
  runParserAttributeHooks catName declName /- builtin -/ false

--- a/stage0/stdlib/Lean/Delaborator.c
+++ b/stage0/stdlib/Lean/Delaborator.c
@ -359,6 +359,7 @@ lean_object* l___regBuiltin_Lean_Delaborator_delabModN___closed__5;
 lean_object* l_Lean_Delaborator_delabMap___lambda__1___closed__4;
 extern lean_object* l_Lean_Elab_Level_elabLevel___main___closed__6;
 lean_object* l_Lean_Delaborator_delabSort___closed__7;
+extern lean_object* l_Lean_Elab_Term_tryCoe___closed__4;
 lean_object* l_Lean_Delaborator_annotateCurPos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabModN___closed__3;
 lean_object* l_Lean_Delaborator_HasOrelse___closed__1;
@ -1163,7 +1164,6 @@ lean_object* l_Lean_Delaborator_delabNot___lambda__1___closed__2;
 lean_object* l_Lean_Delaborator_delabAndM___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Delaborator_delabOfNat___closed__1;
 lean_object* l_Lean_getPPBinderTypes___boxed(lean_object*);
-extern lean_object* l_Lean_Elab_Term_tryCoe___closed__3;
 lean_object* l_ReaderT_bind___at_Lean_Level_quote___main___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@ -19633,7 +19633,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Delaborator_getExprKind___closed__5;
-x_2 = l_Lean_Elab_Term_tryCoe___closed__3;
+x_2 = l_Lean_Elab_Term_tryCoe___closed__4;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
--- a/stage0/stdlib/Lean/Elab/Command.c
+++ b/stage0/stdlib/Lean/Elab/Command.c
@ -120,7 +120,6 @@ lean_object* l_Lean_Elab_Command_elabInitQuot___rarg___boxed(lean_object*, lean_
 lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Command_elabOpenRenaming___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_ensureNoUnassignedMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_addMessageContextPartial___at_Lean_Elab_Command_Lean_AddMessageContext___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__3;
 lean_object* l_Lean_ofExcept___at_Lean_Elab_Command_elabEvalUnsafe___spec__3(lean_object*);
 lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at_Lean_Elab_Command_expandDeclId___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabOpen___closed__2;
@ -708,6 +707,7 @@ lean_object* l_Lean_addAndCompile___at_Lean_Elab_Command_elabEvalUnsafe___spec__
 lean_object* l_Lean_Elab_Command_getRef___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_monadInhabited___rarg(lean_object*, lean_object*);
 lean_object* lean_add_decl(lean_object*, lean_object*);
+extern lean_object* l_Lean_Elab_Term_tryCoe___closed__3;
 lean_object* _init_l_Lean_Elab_Command_Scope_inhabited___closed__1() {
 _start:
 {
@ -15953,7 +15953,7 @@ _start:
 lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
 x_12 = l_Lean_Elab_Command_elabEvalUnsafe___lambda__2___closed__1;
 x_13 = lean_name_mk_string(x_1, x_12);
-x_14 = l_Lean_Parser_declareBuiltinParser___closed__3;
+x_14 = l_Lean_Elab_Term_tryCoe___closed__3;
 lean_inc(x_2);
 x_15 = lean_array_push(x_14, x_2);
 lean_inc(x_4);
--- a/stage0/stdlib/Lean/Elab/LetRec.c
+++ b/stage0/stdlib/Lean/Elab/LetRec.c
@ -36,7 +36,6 @@ extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3_
 lean_object* lean_private_to_user_name(lean_object*);
 extern lean_object* l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
 lean_object* l_Lean_Meta_mkLambdaFVars___at___private_Lean_Elab_Term_15__elabImplicitLambdaAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_ReaderT_Monad___rarg(lean_object*);
 lean_object* l___private_Lean_Elab_LetRec_5__abortIfContainsSyntheticSorry(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withLetDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
@ -85,13 +84,13 @@ extern lean_object* l_Lean_mkAppStx___closed__6;
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_LetRec_1__mkLetRecDeclView___spec__7___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabTermEnsuringType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Meta_Basic_12__withNewLocalInstancesImp___main___rarg___closed__3;
 lean_object* l___private_Lean_Meta_Basic_21__forallBoundedTelescopeImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_applyAttributesImp(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_LetRec_2__withAuxLocalDeclsAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_LetRec_1__mkLetRecDeclView___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_termElabAttribute;
 lean_object* l_Lean_Meta_mkLambdaFVars___at___private_Lean_Elab_Term_15__elabImplicitLambdaAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Parser_Extension_12__ParserAttribute_add___closed__1;
 lean_object* l_Lean_Syntax_isIdOrAtom_x3f(lean_object*);
 extern lean_object* l_Lean_Elab_elabAttr___rarg___closed__3;
 uint8_t l_Lean_isAttribute(lean_object*, lean_object*);
@ -126,14 +125,12 @@ lean_object* l___private_Lean_Elab_LetRec_3__withAuxLocalDecls___rarg(lean_objec
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_LetRec_2__withAuxLocalDeclsAux(lean_object*);
 extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3;
-lean_object* l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__2;
 lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Util_4__expandMacro_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Term_elabLetRec___closed__2;
 lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkForallFVars___at_Lean_Elab_Term_elabForall___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_LetRec_1__mkLetRecDeclView___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__1;
 lean_object* l_Lean_Elab_throwAbort___at_Lean_Elab_Term_ensureNoUnassignedMVars___spec__2___rarg(lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_LetRec_1__mkLetRecDeclView___spec__7___closed__2;
 lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2021,24 +2018,6 @@ return x_24;
 }
 }
 }
-lean_object* _init_l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__1() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = l___private_Lean_Parser_Extension_12__ParserAttribute_add___closed__1;
-x_2 = l_ReaderT_Monad___rarg(x_1);
-return x_2;
-}
-}
-lean_object* _init_l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__2() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__1;
-x_2 = l_ReaderT_Monad___rarg(x_1);
-return x_2;
-}
-}
 lean_object* l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
@ -2047,7 +2026,7 @@ x_9 = lean_ctor_get(x_1, 0);
 lean_inc(x_9);
 lean_dec(x_1);
 x_10 = x_9;
-x_11 = l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__2;
+x_11 = l___private_Lean_Meta_Basic_12__withNewLocalInstancesImp___main___rarg___closed__3;
 x_12 = lean_unsigned_to_nat(0u);
 x_13 = lean_alloc_closure((void*)(l_Array_umapMAux___main___at___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___spec__2), 10, 3);
 lean_closure_set(x_13, 0, x_11);
@ -2584,10 +2563,6 @@ l_Array_umapMAux___main___at___private_Lean_Elab_LetRec_1__mkLetRecDeclView___sp
 lean_mark_persistent(l_Array_umapMAux___main___at___private_Lean_Elab_LetRec_1__mkLetRecDeclView___spec__7___closed__2);
 l_Array_umapMAux___main___at___private_Lean_Elab_LetRec_1__mkLetRecDeclView___spec__7___closed__3 = _init_l_Array_umapMAux___main___at___private_Lean_Elab_LetRec_1__mkLetRecDeclView___spec__7___closed__3();
 lean_mark_persistent(l_Array_umapMAux___main___at___private_Lean_Elab_LetRec_1__mkLetRecDeclView___spec__7___closed__3);
-l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__1 = _init_l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__1();
-lean_mark_persistent(l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__1);
-l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__2 = _init_l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__2();
-lean_mark_persistent(l___private_Lean_Elab_LetRec_4__elabLetRecDeclValues___closed__2);
 l___regBuiltin_Lean_Elab_Term_elabLetRec___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabLetRec___closed__1();
 lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabLetRec___closed__1);
 l___regBuiltin_Lean_Elab_Term_elabLetRec___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_elabLetRec___closed__2();
--- a/stage0/stdlib/Lean/Elab/StructInst.c
+++ b/stage0/stdlib/Lean/Elab/StructInst.c
@ -112,7 +112,6 @@ uint8_t l_List_foldr___main___at_Lean_Elab_Term_StructInst_Struct_allDefault___m
 lean_object* l_Lean_Elab_Term_StructInst_FieldLHS_inhabited___closed__1;
 lean_object* l___private_Lean_Elab_StructInst_16__mkSubstructSource___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__3;
 lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_10__expandParentFields___spec__2___closed__5;
 lean_object* l_List_foldlM___main___at___private_Lean_Elab_StructInst_12__mkFieldMap___spec__10___closed__2;
 lean_object* l_Lean_Elab_Term_StructInst_Struct_ref(lean_object*);
@ -585,6 +584,7 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27;
 lean_object* l_monadInhabited___rarg(lean_object*, lean_object*);
 uint8_t l_Lean_Syntax_isIdent(lean_object*);
+extern lean_object* l_Lean_Elab_Term_tryCoe___closed__3;
 lean_object* l___private_Lean_Elab_StructInst_13__isSimpleField_x3f(lean_object*);
 lean_object* l_Lean_Elab_Term_StructInst_expandStructInstExpectedType(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
@ -13890,7 +13890,7 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_obj
 x_3 = l_System_FilePath_dirName___closed__1;
 x_4 = l_Lean_mkAtomFrom(x_1, x_3);
 x_5 = l_Lean_mkIdentFrom(x_1, x_2);
-x_6 = l_Lean_Parser_declareBuiltinParser___closed__3;
+x_6 = l_Lean_Elab_Term_tryCoe___closed__3;
 x_7 = lean_array_push(x_6, x_1);
 x_8 = lean_array_push(x_7, x_4);
 x_9 = lean_array_push(x_8, x_5);
--- a/stage0/stdlib/Lean/Elab/Tactic/Induction.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Induction.c
@ -84,7 +84,6 @@ lean_object* l___private_Lean_Elab_Tactic_Induction_5__getGeneralizingFVarIds(le
 extern lean_object* l_Lean_Name_inhabited;
 lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__1___closed__1;
 lean_object* l___private_Lean_Elab_Tactic_Induction_15__processResult___closed__4;
-extern lean_object* l_List_forM___main___at___private_Lean_Parser_Extension_12__ParserAttribute_add___spec__1___lambda__1___closed__5;
 lean_object* l_List_foldlM___main___at___private_Lean_Elab_Tactic_Induction_13__getRecInfoDefault___spec__3___lambda__1___closed__1;
 lean_object* l_List_foldlM___main___at___private_Lean_Elab_Tactic_Induction_13__getRecInfoDefault___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_inferType___at___private_Lean_Meta_InferType_1__inferAppType___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -282,6 +281,7 @@ lean_object* l_Lean_Elab_Tactic_elabTerm___boxed(lean_object*, lean_object*, lea
 lean_object* l_Nat_foldMAux___main___at___private_Lean_Elab_Tactic_Induction_15__processResult___spec__1___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Induction_8__getAltName___boxed(lean_object*);
 extern lean_object* l___private_Lean_Elab_Tactic_Basic_2__expandTacticMacroFns___main___closed__6;
+extern lean_object* l_List_forM___main___at___private_Lean_Parser_Extension_12__ParserAttribute_add___spec__1___closed__5;
 lean_object* l_Lean_Elab_Tactic_liftMetaTacticAux___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Lean_Elab_Util_5__regTraceClasses___closed__1;
 lean_object* l_Lean_Meta_induction(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3080,7 +3080,7 @@ x_31 = l_Lean_Elab_Tactic_getRecFromUsing___closed__6;
 x_32 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_32, 0, x_31);
 lean_ctor_set(x_32, 1, x_30);
-x_33 = l_List_forM___main___at___private_Lean_Parser_Extension_12__ParserAttribute_add___spec__1___lambda__1___closed__5;
+x_33 = l_List_forM___main___at___private_Lean_Parser_Extension_12__ParserAttribute_add___spec__1___closed__5;
 x_34 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_34, 0, x_32);
 lean_ctor_set(x_34, 1, x_33);
--- a/stage0/stdlib/Lean/Elab/Tactic/Rewrite.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Rewrite.c
@ -30,7 +30,6 @@ extern lean_object* l___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___closed__
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at_Lean_Elab_Tactic_evalRewrite___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_rewrite___closed__2;
-extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__3;
 lean_object* lean_local_ctx_find_from_user_name(lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
@ -104,6 +103,7 @@ lean_object* l_Lean_Elab_Tactic_evalRewrite___boxed(lean_object*, lean_object*,
 lean_object* l_Lean_Elab_Tactic_expandRewriteTactic(lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at_Lean_Elab_Tactic_evalRewrite___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Elab_Term_tryCoe___closed__3;
 lean_object* _init_l_Array_umapMAux___main___at_Lean_Elab_Tactic_expandRewriteTactic___spec__1___closed__1() {
 _start:
 {
@ -146,7 +146,7 @@ x_9 = lean_array_fset(x_3, x_2, x_8);
 x_10 = x_7;
 x_11 = l_Array_umapMAux___main___at_Lean_Elab_Tactic_expandRewriteTactic___spec__1___closed__2;
 x_12 = l_Lean_mkAtomFrom(x_10, x_11);
-x_13 = l_Lean_Parser_declareBuiltinParser___closed__3;
+x_13 = l_Lean_Elab_Term_tryCoe___closed__3;
 x_14 = lean_array_push(x_13, x_12);
 x_15 = lean_array_push(x_14, x_10);
 lean_inc(x_1);
--- a/stage0/stdlib/Lean/Elab/Term.c
+++ b/stage0/stdlib/Lean/Elab/Term.c
@ -169,7 +169,6 @@ lean_object* l_Lean_Elab_Term_ensureNoUnassignedMVars(lean_object*, lean_object*
 lean_object* l_Lean_Meta_mkFreshExprMVar___at_Lean_Elab_Term_tryCoe___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_16__elabImplicitLambda___main___spec__1(lean_object*);
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__3;
 lean_object* l_Lean_Elab_Term_withoutPostponing(lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__13;
 lean_object* l___private_Lean_Elab_Term_17__elabTermAux___main___closed__1;
@ -827,6 +826,7 @@ lean_object* l_Lean_Elab_Term_ensureHasTypeAux___boxed(lean_object*, lean_object
 uint8_t l_List_isEmpty___rarg(lean_object*);
 lean_object* l_Lean_Elab_Term_mkTermElabAttribute___closed__2;
 lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_tryCoe___closed__5;
 lean_object* l_Lean_Elab_Term_applyResult(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_local_ctx_find(lean_object*, lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
@ -9361,17 +9361,26 @@ return x_3;
 lean_object* _init_l_Lean_Elab_Term_tryCoe___closed__3() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("coe");
-return x_1;
+lean_object* x_1; lean_object* x_2; 
+x_1 = lean_unsigned_to_nat(3u);
+x_2 = lean_mk_empty_array_with_capacity(x_1);
+return x_2;
 }
 }
 lean_object* _init_l_Lean_Elab_Term_tryCoe___closed__4() {
 _start:
 {
+lean_object* x_1; 
+x_1 = lean_mk_string("coe");
+return x_1;
+}
+}
+lean_object* _init_l_Lean_Elab_Term_tryCoe___closed__5() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Elab_Term_tryCoe___closed__3;
+x_2 = l_Lean_Elab_Term_tryCoe___closed__4;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@ -9438,7 +9447,7 @@ lean_ctor_set(x_24, 1, x_23);
 x_25 = l_Lean_Elab_Term_tryCoe___closed__2;
 lean_inc(x_24);
 x_26 = l_Lean_mkConst(x_25, x_24);
-x_27 = l_Lean_Parser_declareBuiltinParser___closed__3;
+x_27 = l_Lean_Elab_Term_tryCoe___closed__3;
 lean_inc(x_2);
 x_28 = lean_array_push(x_27, x_2);
 lean_inc(x_3);
@ -9459,7 +9468,7 @@ lean_inc(x_37);
 x_38 = lean_ctor_get(x_36, 1);
 lean_inc(x_38);
 lean_dec(x_36);
-x_39 = l_Lean_Elab_Term_tryCoe___closed__4;
+x_39 = l_Lean_Elab_Term_tryCoe___closed__5;
 x_40 = l_Lean_mkConst(x_39, x_24);
 x_41 = l_Std_PersistentHashMap_mkCollisionNode___rarg___closed__1;
 lean_inc(x_2);
@ -13403,7 +13412,7 @@ lean_ctor_set(x_91, 0, x_85);
 lean_ctor_set(x_91, 1, x_90);
 x_92 = l_Lean_Elab_Term_tryCoe___closed__2;
 x_93 = l_Lean_mkConst(x_92, x_91);
-x_94 = l_Lean_Parser_declareBuiltinParser___closed__3;
+x_94 = l_Lean_Elab_Term_tryCoe___closed__3;
 lean_inc(x_39);
 x_95 = lean_array_push(x_94, x_39);
 x_96 = l_Lean_Meta_commitWhen___at___private_Lean_Meta_ExprDefEq_1__isDefEqEta___spec__4___closed__1;
@ -14050,7 +14059,7 @@ lean_ctor_set(x_245, 0, x_239);
 lean_ctor_set(x_245, 1, x_244);
 x_246 = l_Lean_Elab_Term_tryCoe___closed__2;
 x_247 = l_Lean_mkConst(x_246, x_245);
-x_248 = l_Lean_Parser_declareBuiltinParser___closed__3;
+x_248 = l_Lean_Elab_Term_tryCoe___closed__3;
 lean_inc(x_193);
 x_249 = lean_array_push(x_248, x_193);
 x_250 = l_Lean_Meta_commitWhen___at___private_Lean_Meta_ExprDefEq_1__isDefEqEta___spec__4___closed__1;
@ -14846,7 +14855,7 @@ lean_ctor_set(x_424, 0, x_418);
 lean_ctor_set(x_424, 1, x_423);
 x_425 = l_Lean_Elab_Term_tryCoe___closed__2;
 x_426 = l_Lean_mkConst(x_425, x_424);
-x_427 = l_Lean_Parser_declareBuiltinParser___closed__3;
+x_427 = l_Lean_Elab_Term_tryCoe___closed__3;
 lean_inc(x_372);
 x_428 = lean_array_push(x_427, x_372);
 x_429 = l_Lean_Meta_commitWhen___at___private_Lean_Meta_ExprDefEq_1__isDefEqEta___spec__4___closed__1;
@ -29022,7 +29031,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l___private_Lean_Elab_Util_5__regTraceClasses___closed__1;
-x_2 = l_Lean_Elab_Term_tryCoe___closed__3;
+x_2 = l_Lean_Elab_Term_tryCoe___closed__4;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@ -29405,6 +29414,8 @@ l_Lean_Elab_Term_tryCoe___closed__3 = _init_l_Lean_Elab_Term_tryCoe___closed__3(
 lean_mark_persistent(l_Lean_Elab_Term_tryCoe___closed__3);
 l_Lean_Elab_Term_tryCoe___closed__4 = _init_l_Lean_Elab_Term_tryCoe___closed__4();
 lean_mark_persistent(l_Lean_Elab_Term_tryCoe___closed__4);
+l_Lean_Elab_Term_tryCoe___closed__5 = _init_l_Lean_Elab_Term_tryCoe___closed__5();
+lean_mark_persistent(l_Lean_Elab_Term_tryCoe___closed__5);
 l___private_Lean_Elab_Term_4__isMonad_x3f___closed__1 = _init_l___private_Lean_Elab_Term_4__isMonad_x3f___closed__1();
 lean_mark_persistent(l___private_Lean_Elab_Term_4__isMonad_x3f___closed__1);
 l___private_Lean_Elab_Term_4__isMonad_x3f___closed__2 = _init_l___private_Lean_Elab_Term_4__isMonad_x3f___closed__2();
--- a/stage0/stdlib/Lean/Parser/Basic.c
+++ b/stage0/stdlib/Lean/Parser/Basic.c
--- a/stage0/stdlib/Lean/Parser/Command.c
+++ b/stage0/stdlib/Lean/Parser/Command.c
@ -425,7 +425,7 @@ lean_object* l_Lean_Parser_Term_quot_formatter___closed__1;
 lean_object* l_Lean_Parser_Command_example___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Command_attribute___closed__10;
 lean_object* l_Lean_Parser_Command_open_parenthesizer___closed__3;
-lean_object* l_Lean_Parser_addBuiltinParser(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_addBuiltinParser(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Lean_Parser_Command_declId_formatter___closed__1;
 lean_object* l_Lean_Parser_Command_structFields;
@ -2947,13 +2947,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_quot(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean___kind_term____x40_Lean_Util_Trace___hyg_3____closed__15;
 x_3 = l_Lean_Parser_Term_quot___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Term_quot;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* l_Lean_Parser_commandParser_formatter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -23895,13 +23896,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_declaration(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_declaration___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_declaration;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_docComment_formatter___closed__1() {
@ -29884,13 +29886,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_section(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_section___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_section;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_section_formatter___closed__1() {
@ -30498,13 +30501,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_namespace(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_namespace___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_namespace;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_namespace_formatter___closed__1() {
@ -31182,13 +31186,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_end(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_end___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_end;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_end_formatter___closed__1() {
@ -31773,13 +31778,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_variable(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_variable___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_variable;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_variable_formatter___closed__1() {
@ -32432,13 +32438,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_variables(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_variables___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_variables;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_variables_formatter___closed__1() {
@ -33046,13 +33053,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_universe(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_universe___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_universe;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_universe_formatter___closed__1() {
@ -33680,13 +33688,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_universes(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_universes___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_universes;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_universes_formatter___closed__1() {
@ -34278,13 +34287,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_check(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_check___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_check;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_check_formatter___closed__1() {
@ -34864,13 +34874,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_check__failure(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_check__failure___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_check__failure;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_check__failure_formatter___closed__1() {
@ -35450,13 +35461,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_eval(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_eval___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_eval;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_eval_formatter___closed__1() {
@ -36036,13 +36048,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_synth(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_synth___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_synth;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_synth_formatter___closed__1() {
@ -36572,13 +36585,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_exit(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_exit___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_exit;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_exit_formatter___closed__1() {
@ -37260,13 +37274,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_print(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_print___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_print;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_print_formatter___closed__1() {
@ -38016,13 +38031,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_printAxioms(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_printAxioms___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_printAxioms;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_printAxioms_formatter___closed__1() {
@ -38622,13 +38638,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_resolve__name(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_resolve__name___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_resolve__name;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_resolve__name_formatter___closed__1() {
@ -39150,13 +39167,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_init__quot(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_init__quot___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_init__quot;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_init__quot_formatter___closed__1() {
@ -40190,13 +40208,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_set__option(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_set__option___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_set__option;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_set__option_formatter___closed__1() {
@ -41623,13 +41642,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_attribute(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_attribute___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_attribute;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_attribute_formatter___closed__1() {
@ -42753,13 +42773,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_export(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_export___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_export;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_export_formatter___closed__1() {
@ -46697,13 +46718,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_open(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_open___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_open;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_openHiding_formatter___closed__1() {
@ -48551,13 +48573,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_mutual(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_mutual___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_mutual;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_mutual_formatter___closed__1() {
@ -49052,13 +49075,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_in(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_in___elambda__1___closed__2;
 x_4 = 0;
 x_5 = l_Lean_Parser_Command_in;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_in_formatter___closed__1() {
--- a/stage0/stdlib/Lean/Parser/Extension.c
+++ b/stage0/stdlib/Lean/Parser/Extension.c
--- a/stage0/stdlib/Lean/Parser/Level.c
+++ b/stage0/stdlib/Lean/Parser/Level.c
@ -88,7 +88,7 @@ lean_object* l_Lean_Parser_ParserState_mkTrailingNode(lean_object*, lean_object*
 lean_object* l_Lean_Parser_Level_hole___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__18;
 lean_object* l_Lean_Parser_mkAntiquot_formatter___closed__8;
-lean_object* l_Lean_Parser_addBuiltinParser(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_addBuiltinParser(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__25;
 lean_object* lean_string_append(lean_object*, lean_object*);
@ -972,13 +972,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_paren(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__2;
 x_3 = l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___lambda__1___closed__3;
 x_4 = 1;
 x_5 = l_Lean_Parser_Level_paren;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* l_Lean_Parser_dollarSymbol_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -2562,13 +2563,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_max(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Level_max___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Level_max;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_max_formatter___closed__1() {
@ -3111,13 +3113,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_imax(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Level_imax___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Level_imax;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_imax_formatter___closed__1() {
@ -3631,13 +3634,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_hole(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Level_hole___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Level_hole;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_hole_formatter___closed__1() {
@ -3847,13 +3851,14 @@ return x_3;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_num(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__2;
 x_3 = l___regBuiltinParser_Lean_Parser_Level_num___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Level_num;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_numLit_formatter___closed__1() {
@ -4079,13 +4084,14 @@ return x_3;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_ident(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__2;
 x_3 = l___regBuiltinParser_Lean_Parser_Level_ident___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Level_ident;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_ident_formatter___closed__1() {
@ -4454,13 +4460,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_addLit(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
 x_4 = 0;
 x_5 = l_Lean_Parser_Level_addLit;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_addLit_formatter___closed__1() {
--- a/stage0/stdlib/Lean/Parser/Module.c
+++ b/stage0/stdlib/Lean/Parser/Module.c
@ -161,13 +161,13 @@ lean_object* l_Lean_Parser_Module_header_parenthesizer___closed__2;
 lean_object* l___private_Lean_Parser_Module_4__testModuleParserAux___main___closed__1;
 lean_object* l_Lean_Parser_Module_import___closed__1;
 lean_object* l_Std_PersistentArray_forMAux___main___at___private_Lean_Parser_Module_4__testModuleParserAux___main___spec__4___boxed(lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
 lean_object* l___private_Lean_Parser_Module_4__testModuleParserAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Module_import_formatter___closed__7;
 lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 uint8_t l_Std_PersistentArray_isEmpty___rarg(lean_object*);
 lean_object* l_Lean_Parser_Module_header_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Trie_Inhabited(lean_object*);
+extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
 lean_object* l_IO_FS_readFile___at_Lean_Parser_parseFile___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Module_module;
@ -3206,7 +3206,7 @@ _start:
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
-x_3 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
+x_3 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_3);
 lean_ctor_set(x_4, 1, x_2);
--- a/stage0/stdlib/Lean/Parser/Syntax.c
+++ b/stage0/stdlib/Lean/Parser/Syntax.c
@ -263,7 +263,7 @@ lean_object* l_Lean_Parser_Command_mixfix___elambda__1(lean_object*, lean_object
 lean_object* l_Lean_Parser_Syntax_cat___closed__2;
 lean_object* l_Lean_Parser_Command_notation___closed__10;
 lean_object* l_Lean_Parser_Command_identPrec_parenthesizer___closed__2;
-lean_object* l_Lean_Parser_addBuiltinParser(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_addBuiltinParser(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__1;
 lean_object* l___regBuiltin_Lean_Parser_Syntax_atom_formatter___closed__1;
 lean_object* l___regBuiltin_Lean_Parser_Syntax_many_formatter(lean_object*);
@ -3098,13 +3098,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_paren(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_paren___elambda__1___closed__3;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_paren;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* l_Lean_Parser_syntaxParser_formatter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -3607,13 +3608,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_cat(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_cat___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_cat;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_maxSymbol_formatter___closed__1() {
@ -4279,13 +4281,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_atom(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_atom___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_atom;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_atom_formatter___closed__1() {
@ -4652,13 +4655,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_num(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_num___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_num;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_num_formatter___closed__1() {
@ -5035,13 +5039,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_str(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_str___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_str;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_str_formatter___closed__1() {
@ -5418,13 +5423,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_char(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_char___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_char;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_char_formatter___closed__1() {
@ -5801,13 +5807,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_ident(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_ident___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_ident;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_ident_formatter___closed__1() {
@ -6262,13 +6269,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_try(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_try___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_try;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_try_formatter___closed__1() {
@ -6747,13 +6755,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_lookahead(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_lookahead___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_lookahead;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_lookahead_formatter___closed__1() {
@ -7256,13 +7265,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_sepBy(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_sepBy___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_sepBy;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_sepBy_formatter___closed__1() {
@ -7787,13 +7797,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_sepBy1(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_sepBy1___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_sepBy1;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_sepBy1_formatter___closed__1() {
@ -8242,13 +8253,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_notFollowedBy(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_notFollowedBy___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Syntax_notFollowedBy;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_notFollowedBy_formatter___closed__1() {
@ -8544,13 +8556,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_optional(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
 x_4 = 0;
 x_5 = l_Lean_Parser_Syntax_optional;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* l_Lean_Parser_Syntax_optional_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -8770,13 +8783,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_many(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_many___elambda__1___closed__2;
 x_4 = 0;
 x_5 = l_Lean_Parser_Syntax_many;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* l_Lean_Parser_Syntax_many_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -9046,13 +9060,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_many1(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_many1___elambda__1___closed__2;
 x_4 = 0;
 x_5 = l_Lean_Parser_Syntax_many1;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_many1_formatter___closed__1() {
@ -9315,13 +9330,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Syntax_orelse(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_categoryParserFnImpl___closed__4;
 x_3 = l_Lean_Parser_Syntax_orelse___elambda__1___closed__1;
 x_4 = 0;
 x_5 = l_Lean_Parser_Syntax_orelse;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Syntax_orelse_formatter___closed__1() {
@ -10023,13 +10039,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_stx_quot(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean___kind_term____x40_Lean_Util_Trace___hyg_3____closed__15;
 x_3 = l_Lean_Parser_Term_stx_quot___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Term_stx_quot;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Term_stx_quot_formatter___closed__1() {
@ -13258,13 +13275,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_mixfix(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_mixfix___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_mixfix;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_prefix_formatter___closed__1() {
@ -14730,13 +14748,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_reserve(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_reserve___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_reserve;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_reserve_formatter___closed__1() {
@ -16690,13 +16709,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_notation(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_notation___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_notation;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_identPrec_formatter___closed__1() {
@ -17655,13 +17675,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_macro__rules(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_macro__rules___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_macro__rules;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_optKind_formatter___closed__1() {
@ -18679,13 +18700,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_syntax(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_syntax___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_syntax;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_syntax_formatter___closed__1() {
@ -19565,13 +19587,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_syntaxAbbrev(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_syntaxAbbrev___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_syntaxAbbrev;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_syntaxAbbrev_formatter___closed__1() {
@ -20197,13 +20220,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_syntaxCat(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_syntaxCat;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_syntaxCat_formatter___closed__1() {
@ -23358,13 +23382,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_macro(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_macro___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_macro;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_macroArgSimple_formatter___closed__1() {
@ -25330,13 +25355,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_elab__rules(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_elab__rules___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_elab__rules;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_elab__rules_formatter___closed__1() {
@ -26685,13 +26711,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Command_elab(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_formatCommand___closed__2;
 x_3 = l_Lean_Parser_Command_elab___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_elab;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* l_Lean_Parser_Command_elabHead_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
--- a/stage0/stdlib/Lean/Parser/Tactic.c
+++ b/stage0/stdlib/Lean/Parser/Tactic.c
@ -342,7 +342,7 @@ extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean
 lean_object* l_Lean_Parser_Tactic_failIfSuccess___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Tactic_refine_x21___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_exact___closed__1;
-lean_object* l_Lean_Parser_addBuiltinParser(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_addBuiltinParser(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Parser_Tactic_apply_formatter___closed__1;
 lean_object* l_Lean_Parser_Tactic_rewrite_parenthesizer___closed__4;
 lean_object* l_Lean_Parser_Tactic_rewriteSeq_parenthesizer___closed__5;
@ -2793,13 +2793,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_intro(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_intro___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_intro;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_intro_formatter___closed__1() {
@ -3411,13 +3412,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_intros(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_intros___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_intros;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_ident_x27_formatter___closed__1() {
@ -4068,13 +4070,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_revert(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_revert___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_revert;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_revert_formatter___closed__1() {
@ -4611,13 +4614,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_clear(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_clear___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_clear;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_clear_formatter___closed__1() {
@ -5114,13 +5118,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_subst(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_subst___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_subst;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_subst_formatter___closed__1() {
@ -5517,13 +5522,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_assumption(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_assumption___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_assumption;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_assumption_formatter___closed__1() {
@ -5968,13 +5974,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_apply(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_apply___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_apply;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_apply_formatter___closed__1() {
@ -6443,13 +6450,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_exact(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_exact___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_exact;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_exact_formatter___closed__1() {
@ -6906,13 +6914,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_refine(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_refine___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_refine;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_refine_formatter___closed__1() {
@ -7369,13 +7378,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_refine_x21(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_refine_x21___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_refine_x21;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_refine_x21_formatter___closed__1() {
@ -7929,13 +7939,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_case(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_case___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_case;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_case_formatter___closed__1() {
@ -8457,13 +8468,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_allGoals(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_allGoals___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_allGoals;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_allGoals_formatter___closed__1() {
@ -8872,13 +8884,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_skip(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_skip___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_skip;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_skip_formatter___closed__1() {
@ -9263,13 +9276,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_done(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_done___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_done;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_done_formatter___closed__1() {
@ -9654,13 +9668,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_admit(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_admit___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_admit;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_admit_formatter___closed__1() {
@ -10045,13 +10060,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_traceState(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_traceState___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_traceState;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_traceState_formatter___closed__1() {
@ -10501,13 +10517,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_failIfSuccess(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_failIfSuccess___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_failIfSuccess;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_failIfSuccess_formatter___closed__1() {
@ -11683,13 +11700,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_generalize(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_generalize;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_generalize_formatter___closed__1() {
@ -14061,13 +14079,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_change(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_change___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_change;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_locationWildcard_formatter___closed__1() {
@ -15335,13 +15354,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_changeWith(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_changeWith___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_changeWith;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_changeWith_formatter___closed__1() {
@ -17628,13 +17648,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_rewrite(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_rewrite___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_rewrite;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_rwRule_formatter___closed__1() {
@ -18521,13 +18542,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_rewriteSeq(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_rewriteSeq___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_rewriteSeq;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_rwRuleSeq_formatter___closed__1() {
@ -22667,13 +22689,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_induction(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_induction___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_induction;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_majorPremise_formatter___closed__1() {
@ -23837,13 +23860,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_cases(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_cases___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_cases;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_cases_formatter___closed__1() {
@ -26504,13 +26528,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_match(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_match___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_match;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_matchAlt_formatter___closed__1() {
@ -27250,13 +27275,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_introMatch(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_introMatch___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_introMatch;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_introMatch_formatter___closed__1() {
@ -28003,13 +28029,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_injection(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_injection___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_injection;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_withIds_formatter___closed__1() {
@ -28787,13 +28814,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_paren(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_paren;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_seq1_formatter___closed__1() {
@ -29561,13 +29589,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_nestedTacticBlockCurly(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_nestedTacticBlockCurly;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_seq_formatter___closed__1() {
@ -30032,13 +30061,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_orelse(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
 x_4 = 0;
 x_5 = l_Lean_Parser_Tactic_orelse;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_orelse_formatter___closed__1() {
@ -30516,13 +30546,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_have(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_have___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_have;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_have_formatter___closed__1() {
@ -31034,13 +31065,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_suffices(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_suffices___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_suffices;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_suffices_formatter___closed__1() {
@ -31556,13 +31588,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_show(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_show___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_show;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_show_formatter___closed__1() {
@ -32059,13 +32092,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_let(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_let___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_let;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_let_formatter___closed__1() {
@ -32562,13 +32596,14 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_let_x21(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
 x_3 = l_Lean_Parser_Tactic_let_x21___elambda__1___closed__1;
 x_4 = 1;
 x_5 = l_Lean_Parser_Tactic_let_x21;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+x_6 = lean_unsigned_to_nat(0u);
+x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
+return x_7;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_let_x21_formatter___closed__1() {
--- a/stage0/stdlib/Lean/Parser/Term.c
+++ b/stage0/stdlib/Lean/Parser/Term.c
--- a/stage0/stdlib/Lean/PrettyPrinter/Formatter.c
+++ b/stage0/stdlib/Lean/PrettyPrinter/Formatter.c
@ -116,6 +116,7 @@ lean_object* l_Lean_throwError___at_Lean_PrettyPrinter_Formatter_formatterForKin
 lean_object* l_Lean_PrettyPrinter_Formatter_notFollowedBy_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_throwBacktrack___rarg(lean_object*);
+lean_object* l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__5;
 lean_object* l_Lean_PrettyPrinter_Formatter_optional_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkFormatterAttribute___closed__9;
 lean_object* l_Lean_PrettyPrinter_Formatter_getStack___boxed(lean_object*);
@ -252,7 +253,6 @@ lean_object* l_Lean_PrettyPrinter_formatCommand___closed__1;
 lean_object* l_Lean_PrettyPrinter_Formatter_identNoAntiquot_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_MonadTraverser_getCur___at_Lean_PrettyPrinter_Formatter_visitArgs___spec__1___boxed(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_symbolNoWs_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Parser_Extension_12__ParserAttribute_add___closed__1;
 lean_object* l_Lean_PrettyPrinter_Formatter_FormatterM_monadTraverser___closed__3;
 lean_object* l_Lean_PrettyPrinter_Formatter_withPosition_formatter___closed__1;
 extern lean_object* l_Lean_formatDataValue___closed__2;
@ -398,6 +398,7 @@ lean_object* l_Lean_Name_components(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_unicodeSymbol_formatter___closed__2;
 lean_object* l_Lean_PrettyPrinter_Formatter_andthen_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_checkKind___closed__1;
+extern lean_object* l_Lean_MetavarContext_MkBinding_mkBinding___closed__1;
 lean_object* l_Lean_PrettyPrinter_Formatter_ppLine_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Formatter_pushTokenCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkCombinatorFormatterAttribute___closed__2;
@ -3444,7 +3445,7 @@ lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___clo
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l___private_Lean_Parser_Extension_12__ParserAttribute_add___closed__1;
+x_1 = l_Lean_MetavarContext_MkBinding_mkBinding___closed__1;
 x_2 = l_ReaderT_Monad___rarg(x_1);
 return x_2;
 }
@ -3454,12 +3455,21 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; 
 x_1 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__1;
+x_2 = l_ReaderT_Monad___rarg(x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__2;
 x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___lambda__1___boxed), 7, 1);
 lean_closure_set(x_2, 0, x_1);
 return x_2;
 }
 }
-lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__3() {
+lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__4() {
 _start:
 {
 lean_object* x_1; 
@ -3467,12 +3477,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Syntax_MonadTraverser_getCur___at_Lean_P
 return x_1;
 }
 }
-lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__4() {
+lean_object* _init_l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__3;
-x_2 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__2;
+x_1 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__4;
+x_2 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__3;
 x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_PrettyPrinter_Formatter_categoryParser_formatter___spec__4___rarg), 7, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
@ -3560,7 +3570,7 @@ else
 lean_object* x_29; lean_object* x_30; 
 lean_dec(x_10);
 lean_dec(x_1);
-x_29 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__4;
+x_29 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__5;
 lean_inc(x_5);
 lean_inc(x_4);
 lean_inc(x_3);
@ -7480,6 +7490,8 @@ l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__3 = _init_l_Le
 lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__3);
 l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__4 = _init_l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__4();
 lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__4);
+l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__5 = _init_l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__5();
+lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__5);
 l_Lean_PrettyPrinter_Formatter_checkKind___lambda__1___closed__1 = _init_l_Lean_PrettyPrinter_Formatter_checkKind___lambda__1___closed__1();
 lean_mark_persistent(l_Lean_PrettyPrinter_Formatter_checkKind___lambda__1___closed__1);
 l_Lean_PrettyPrinter_Formatter_checkKind___lambda__1___closed__2 = _init_l_Lean_PrettyPrinter_Formatter_checkKind___lambda__1___closed__2();
--- a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
+++ b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
@ -277,6 +277,7 @@ lean_object* l_Lean_Syntax_MonadTraverser_goRight___at_Lean_PrettyPrinter_Parent
 lean_object* l___regBuiltin_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer(lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_MonadTraverser_getCur___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__1(lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__2___closed__6;
@ -307,7 +308,6 @@ lean_object* l_Lean_Syntax_Traverser_fromSyntax(lean_object*);
 lean_object* l_Lean_PrettyPrinter_mkCombinatorParenthesizerAttribute___closed__3;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoWsBefore_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getHeadInfo___main(lean_object*);
-extern lean_object* l___private_Lean_Parser_Extension_12__ParserAttribute_add___closed__1;
 lean_object* l_Lean_Syntax_MonadTraverser_goRight___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__8___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_pushNone_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__9;
@ -469,6 +469,7 @@ lean_object* l_Lean_PrettyPrinter_parenthesize___closed__2;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___closed__2;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_addPrecCheck___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Substring_splitOnAux___main___closed__2;
+extern lean_object* l_Lean_MetavarContext_MkBinding_mkBinding___closed__1;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_identNoAntiquot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_notFollowedBy_parenthesizer___rarg(lean_object*);
 lean_object* l_Lean_Syntax_MonadTraverser_getCur___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -3799,7 +3800,7 @@ lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l___private_Lean_Parser_Extension_12__ParserAttribute_add___closed__1;
+x_1 = l_Lean_MetavarContext_MkBinding_mkBinding___closed__1;
 x_2 = l_ReaderT_Monad___rarg(x_1);
 return x_2;
 }
@ -3807,6 +3808,15 @@ return x_2;
 lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__2() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__1;
+x_2 = l_ReaderT_Monad___rarg(x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__3() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
 x_2 = l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__5;
@ -3814,7 +3824,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__3() {
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__4() {
 _start:
 {
 lean_object* x_1; 
@ -3822,37 +3832,37 @@ x_1 = lean_mk_string("parenthesize");
 return x_1;
 }
 }
-lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__4() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__2;
-x_2 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__3;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
 lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__1;
-x_2 = l_PUnit_Inhabited;
-x_3 = l_monadInhabited___rarg(x_1, x_2);
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__3;
+x_2 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__4;
+x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
 lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__6() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__2;
+x_2 = l_PUnit_Inhabited;
+x_3 = l_monadInhabited___rarg(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__7() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__5;
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__6;
 x_2 = lean_alloc_closure((void*)(l_ReaderT_inhabited___rarg___boxed), 2, 1);
 lean_closure_set(x_2, 0, x_1);
 return x_2;
 }
 }
-lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__7() {
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__8() {
 _start:
 {
 lean_object* x_1; 
@ -3860,7 +3870,7 @@ x_1 = lean_mk_string("Lean.PrettyPrinter.Parenthesizer");
 return x_1;
 }
 }
-lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__8() {
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__9() {
 _start:
 {
 lean_object* x_1; 
@ -3868,19 +3878,19 @@ x_1 = lean_mk_string("maybeParenthesize: visited a syntax tree without precedenc
 return x_1;
 }
 }
-lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__9() {
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__10() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__7;
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__8;
 x_2 = lean_unsigned_to_nat(206u);
 x_3 = lean_unsigned_to_nat(4u);
-x_4 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__8;
+x_4 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__9;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
 return x_5;
 }
 }
-lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__10() {
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
@ -3890,7 +3900,7 @@ lean_ctor_set(x_2, 0, x_1);
 return x_2;
 }
 }
-lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11() {
+lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
@ -3949,7 +3959,7 @@ x_30 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_maybeParent
 lean_closure_set(x_30, 0, x_21);
 lean_closure_set(x_30, 1, x_11);
 lean_closure_set(x_30, 2, x_20);
-x_31 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__4;
+x_31 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__5;
 x_32 = l_Lean_MonadTracer_trace___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__2(x_31, x_30, x_5, x_6, x_7, x_8, x_29);
 x_33 = lean_ctor_get(x_32, 1);
 lean_inc(x_33);
@ -3985,8 +3995,8 @@ lean_dec(x_1);
 x_39 = lean_ctor_get(x_36, 1);
 lean_inc(x_39);
 lean_dec(x_36);
-x_40 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__6;
-x_41 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__9;
+x_40 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__7;
+x_41 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__10;
 x_42 = lean_panic_fn(x_40, x_41);
 x_43 = lean_apply_5(x_42, x_5, x_6, x_7, x_8, x_39);
 return x_43;
@ -4526,7 +4536,7 @@ x_163 = lean_ctor_get(x_159, 2);
 lean_dec(x_163);
 x_164 = lean_ctor_get(x_159, 1);
 lean_dec(x_164);
-x_165 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__10;
+x_165 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
 lean_ctor_set(x_159, 4, x_25);
 lean_ctor_set(x_159, 2, x_1);
 lean_ctor_set(x_159, 1, x_165);
@ -4546,7 +4556,7 @@ x_170 = lean_ctor_get_uint8(x_159, sizeof(void*)*5);
 lean_inc(x_169);
 lean_inc(x_168);
 lean_dec(x_159);
-x_171 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__10;
+x_171 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
 x_172 = lean_alloc_ctor(0, 5, 1);
 lean_ctor_set(x_172, 0, x_168);
 lean_ctor_set(x_172, 1, x_171);
@ -4621,7 +4631,7 @@ if (x_192 == 0)
 lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196; uint8_t x_197; 
 x_193 = lean_ctor_get(x_186, 0);
 x_194 = lean_ctor_get(x_186, 1);
-x_195 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
+x_195 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
 lean_inc(x_194);
 lean_ctor_set(x_186, 0, x_195);
 x_196 = l_Lean_Syntax_setHeadInfo(x_180, x_186);
@ -4697,7 +4707,7 @@ lean_inc(x_222);
 lean_inc(x_221);
 lean_inc(x_220);
 lean_dec(x_186);
-x_223 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
+x_223 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
 lean_inc(x_221);
 x_224 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_224, 0, x_223);
@ -4806,7 +4816,7 @@ if (x_254 == 0)
 lean_object* x_255; lean_object* x_256; lean_object* x_257; lean_object* x_258; uint8_t x_259; 
 x_255 = lean_ctor_get(x_248, 0);
 x_256 = lean_ctor_get(x_248, 1);
-x_257 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
+x_257 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
 lean_inc(x_256);
 lean_ctor_set(x_248, 0, x_257);
 x_258 = l_Lean_Syntax_setHeadInfo(x_242, x_248);
@ -4882,7 +4892,7 @@ lean_inc(x_284);
 lean_inc(x_283);
 lean_inc(x_282);
 lean_dec(x_248);
-x_285 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
+x_285 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
 lean_inc(x_283);
 x_286 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_286, 0, x_285);
@ -5008,7 +5018,7 @@ x_325 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_maybeParen
 lean_closure_set(x_325, 0, x_315);
 lean_closure_set(x_325, 1, x_11);
 lean_closure_set(x_325, 2, x_314);
-x_326 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__4;
+x_326 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__5;
 x_327 = l_Lean_MonadTracer_trace___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__2(x_326, x_325, x_5, x_6, x_7, x_8, x_324);
 x_328 = lean_ctor_get(x_327, 1);
 lean_inc(x_328);
@ -5044,8 +5054,8 @@ lean_dec(x_1);
 x_334 = lean_ctor_get(x_331, 1);
 lean_inc(x_334);
 lean_dec(x_331);
-x_335 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__6;
-x_336 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__9;
+x_335 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__7;
+x_336 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__10;
 x_337 = lean_panic_fn(x_335, x_336);
 x_338 = lean_apply_5(x_337, x_5, x_6, x_7, x_8, x_334);
 return x_338;
@ -5456,7 +5466,7 @@ if (lean_is_exclusive(x_411)) {
 lean_dec_ref(x_411);
 x_416 = lean_box(0);
 }
-x_417 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__10;
+x_417 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
 if (lean_is_scalar(x_416)) {
 x_418 = lean_alloc_ctor(0, 5, 1);
 } else {
@ -5543,7 +5553,7 @@ if (lean_is_exclusive(x_432)) {
 lean_dec_ref(x_432);
 x_441 = lean_box(0);
 }
-x_442 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
+x_442 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
 lean_inc(x_439);
 if (lean_is_scalar(x_441)) {
 x_443 = lean_alloc_ctor(0, 3, 0);
@ -5664,7 +5674,7 @@ if (lean_is_exclusive(x_467)) {
 lean_dec_ref(x_467);
 x_476 = lean_box(0);
 }
-x_477 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
+x_477 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
 lean_inc(x_474);
 if (lean_is_scalar(x_476)) {
 x_478 = lean_alloc_ctor(0, 3, 0);
@ -7366,7 +7376,7 @@ lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___close
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__4;
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__5;
 x_2 = l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@ -9335,7 +9345,7 @@ lean_object* l___private_Lean_PrettyPrinter_Parenthesizer_1__regTraceClasses(lea
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__4;
+x_2 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__5;
 x_3 = l_Lean_registerTraceClass(x_2, x_1);
 if (lean_obj_tag(x_3) == 0)
 {
@ -9609,6 +9619,8 @@ l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__10 = _init_l_Lean
 lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__10);
 l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11 = _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11();
 lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11);
+l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12 = _init_l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12();
+lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12);
 l_Lean_PrettyPrinter_Parenthesizer_parenthesizerForKind___closed__1 = _init_l_Lean_PrettyPrinter_Parenthesizer_parenthesizerForKind___closed__1();
 lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_parenthesizerForKind___closed__1);
 l_Lean_PrettyPrinter_Parenthesizer_parenthesizerForKind___closed__2 = _init_l_Lean_PrettyPrinter_Parenthesizer_parenthesizerForKind___closed__2();