chore: update stage0

stage0/src/Lean/Elab/Binders.lean

@@ -40,7 +40,7 @@ structure BinderView :=
 partial def quoteAutoTactic : Syntax → TermElabM Syntax
 | stx@(Syntax.ident _ _ _ _) => throwErrorAt stx "invalic auto tactic, identifier is not allowed"
 | stx@(Syntax.node k args)   =>
-  if Quotation.isAntiquot stx then
+  if stx.isAntiquot then
     throwErrorAt stx "invalic auto tactic, antiquotation is not allowed"
   else do
     empty ← `(Array.empty);

stage0/src/Lean/Elab/Quotation.lean

@@ -26,15 +26,7 @@ namespace Elab
 namespace Term
 namespace Quotation
 
--- quotation node kinds are formed from a unique quotation name plus "quot"
-def isQuot : Syntax → Bool
-| Syntax.node (Name.str _ "quot" _) _ => true
-| _                                   => false
-
--- antiquotation node kinds are formed from the original node kind (if any) plus "antiquot"
-def isAntiquot : Syntax → Bool
-| Syntax.node (Name.str _ "antiquot" _) _ => true
-| _                                       => false
+open Lean.Syntax (isQuot isAntiquot)
 
 -- Antiquotations can be escaped as in `$$x`, which is useful for nesting macros.
 def isEscapedAntiquot (stx : Syntax) : Bool :=

stage0/src/Lean/Elab/Syntax.lean

@@ -250,7 +250,7 @@ def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM
 alts ← alts.mapSepElemsM $ fun alt => do {
   let lhs := alt.getArg 0;
   let pat := lhs.getArg 0;
-  when (!Term.Quotation.isQuot pat) $
+  when (!pat.isQuot) $
     throwUnsupportedSyntax;
   let quot := pat.getArg 1;
   let k' := quot.getKind;
@@ -271,7 +271,7 @@ alts ← alts.mapSepElemsM $ fun alt => do {
 def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind := do
 let lhs := alt.getArg 0;
 let pat := lhs.getArg 0;
-when (!Term.Quotation.isQuot pat) $
+when (!pat.isQuot) $
   throwUnsupportedSyntax;
 let quot := pat.getArg 1;
 pure quot.getKind

stage0/src/Lean/Parser/Basic.lean

@@ -304,14 +304,14 @@ abbrev TrailingParser := Parser
 @[noinline] def epsilonInfo : ParserInfo :=
 { firstTokens := FirstTokens.epsilon }
 
-@[inline] def checkStackTopFn (p : Syntax → Bool) : ParserFn :=
+@[inline] def checkStackTopFn (p : Syntax → Bool) (msg : String) : ParserFn :=
 fun c s =>
   if p s.stxStack.back then s
-  else s.mkUnexpectedError "invalid leading token"
+  else s.mkUnexpectedError msg
 
-@[inline] def checkStackTop (p : Syntax → Bool) : Parser :=
+@[inline] def checkStackTop (p : Syntax → Bool) (msg : String) : Parser :=
 { info := epsilonInfo,
-  fn   := checkStackTopFn p }
+  fn   := checkStackTopFn p msg }
 
 @[inline] def andthenFn (p q : ParserFn) : ParserFn :=
 fun c s =>
@@ -1481,7 +1481,7 @@ def pushNone : Parser :=
 { fn := fun c s => s.pushSyntax mkNullNode }
 
 -- We support two kinds of antiquotations: `$id` and `$(t)`, where `id` is a term identifier and `t` is a term.
-def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbol "(" >> termParser >> ")")
+def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbol "(" >> toggleInsideQuot termParser >> ")")
 def antiquotExpr : Parser       := identNoAntiquot <|> antiquotNestedExpr
 
 /--

stage0/src/Lean/Parser/Command.lean

@@ -22,7 +22,7 @@ categoryParser `command rbp
   `($x $y) will be parsed as an application, not two commands. Use `($x:command $y:command) instead.
   Multiple command will be put in a `null node, but a single command will not (so that you can directly
   match against a quotation in a command kind's elaborator). -/
-@[builtinTermParser] def Term.quot := parser! "`(" >> (termParser <|> many1 commandParser true) >> ")"
+@[builtinTermParser] def Term.quot := parser! "`(" >> toggleInsideQuot (termParser <|> many1 commandParser true) >> ")"
 
 namespace Command
 def commentBody : Parser :=

stage0/src/Lean/Parser/Level.lean

@@ -21,8 +21,8 @@ namespace Level
 @[builtinLevelParser] def max    := parser! nonReservedSymbol "max " true  >> many1 (levelParser maxPrec)
 @[builtinLevelParser] def imax   := parser! nonReservedSymbol "imax " true >> many1 (levelParser maxPrec)
 @[builtinLevelParser] def hole   := parser! "_"
-@[builtinLevelParser] def num    := parser! numLit
-@[builtinLevelParser] def ident  := parser! ident
+@[builtinLevelParser] def num    := checkInsideQuot >> numLit <|> checkOutsideQuot >> parser! numLit
+@[builtinLevelParser] def ident  := checkInsideQuot >> ident <|> checkOutsideQuot >> parser! ident
 @[builtinLevelParser] def addLit := tparser!:65 "+" >> numLit
 
 end Level

stage0/src/Lean/Parser/Term.lean

@@ -43,14 +43,13 @@ checkPrec prec >> symbol sym >> termParser (prec+1)
 def leadPrec := maxPrec - 1
 
 /- Built-in parsers -/
--- NOTE: `checkNoWsBefore` should be used *before* `parser!` so that it is also applied to the generated
--- antiquotation.
-def explicitUniv := checkNoWsBefore "no space before '.{'" >> parser! ".{" >> sepBy1 levelParser ", " >> "}"
-def namedPattern := checkNoWsBefore "no space before '@'" >> parser! "@" >> termParser maxPrec
-@[builtinTermParser] def id := parser! ident >> optional (explicitUniv <|> namedPattern)
-@[builtinTermParser] def num : Parser := parser! numLit
-@[builtinTermParser] def str : Parser := parser! strLit
-@[builtinTermParser] def char : Parser := parser! charLit
+def explicitUniv' := checkNoWsBefore "no space before '.{'" >> parser! ".{" >> sepBy1 levelParser ", " >> "}"
+def namedPattern' := checkNoWsBefore "no space before '@'" >> parser! "@" >> termParser maxPrec
+@[builtinTermParser] def id := checkOutsideQuot >> parser! ident >> optional (explicitUniv' <|> namedPattern')
+@[builtinTermParser] def ident := checkInsideQuot >> Parser.ident
+@[builtinTermParser] def num : Parser := checkInsideQuot >> numLit <|> checkOutsideQuot >> parser! numLit
+@[builtinTermParser] def str : Parser := checkInsideQuot >> strLit <|> checkOutsideQuot >> parser! strLit
+@[builtinTermParser] def char : Parser := checkInsideQuot >> charLit <|> checkOutsideQuot >> parser! charLit
 @[builtinTermParser] def type := parser! "Type" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec)
 @[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec)
 @[builtinTermParser] def prop := parser! "Prop"
@@ -155,6 +154,15 @@ def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
 @[builtinTermParser] def arrow    := tparser! unicodeInfixR " → " " -> " 25
 @[builtinTermParser] def arrayRef := tparser! symbolNoWs "[" >> termParser >>"]"
 
+def isIdent (stx : Syntax) : Bool :=
+-- antiquotations should also be allowed where an identifier is expected
+stx.isAntiquot || stx.isIdent
+
+-- NOTE: `check*` should be used *before* `tparser!` so that it is also applied to the generated
+-- antiquotation.
+@[builtinTermParser] def explicitUniv : TrailingParser := checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> tparser! ".{" >> sepBy1 levelParser ", " >> "}"
+@[builtinTermParser] def namedPattern : TrailingParser := checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> tparser! "@" >> termParser maxPrec
+
 @[builtinTermParser] def dollar     := tparser!:0 try (dollarSymbol >> checkWsBefore "expected space") >> termParser 0
 @[builtinTermParser] def dollarProj := tparser!:0 " $. " >> (fieldIdx <|> ident)
 
@@ -209,12 +217,12 @@ def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
 @[builtinTermParser] def tacticBlock := parser! "begin " >> Tactic.seq >> "end"
 @[builtinTermParser] def byTactic    := parser!:leadPrec "by " >> Tactic.nonEmptySeq
 
-@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> funBinder >> ")"
+@[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|"  >> toggleInsideQuot funBinder >> ")"
 end Term
 
 -- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.quot`
-@[builtinTermParser] def Tactic.quot : Parser := parser! "`(tactic|" >> sepBy1 tacticParser "; " true true >> ")"
-@[builtinTermParser] def Level.quot  : Parser := parser! "`(level|" >> levelParser >> ")"
+@[builtinTermParser] def Tactic.quot : Parser := parser! "`(tactic|" >> toggleInsideQuot (sepBy1 tacticParser "; " true true) >> ")"
+@[builtinTermParser] def Level.quot  : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")"
 
 end Parser
 end Lean

stage0/src/Lean/Syntax.lean

@@ -20,6 +20,16 @@ def Syntax.isMissing : Syntax → Bool
 | Syntax.missing => true
 | _ => false
 
+-- quotation node kinds are formed from a unique quotation name plus "quot"
+def Syntax.isQuot : Syntax → Bool
+| Syntax.node (Name.str _ "quot" _) _ => true
+| _                                   => false
+
+-- antiquotation node kinds are formed from the original node kind (if any) plus "antiquot"
+def Syntax.isAntiquot : Syntax → Bool
+| Syntax.node (Name.str _ "antiquot" _) _ => true
+| _                                       => false
+
 inductive IsNode : Syntax → Prop
 | mk (kind : SyntaxNodeKind) (args : Array Syntax) : IsNode (Syntax.node kind args)
 

stage0/stdlib/Lean/Delaborator.c

@@ -117,7 +117,6 @@ lean_object* l_Lean_SMap_empty___at_Lean_Delaborator_delabAttribute___spec__1;
 lean_object* l_Lean_Delaborator_mkDelabAttribute___lambda__1___closed__1;
 lean_object* l___regBuiltin_Lean_Delaborator_delabForall___closed__1;
 lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
-extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__5;
 uint8_t l_Lean_getPPStructureProjections(lean_object*);
 lean_object* l_Lean_Delaborator_DelabM_monadQuotation___closed__1;
 extern lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__2;
@@ -161,7 +160,6 @@ lean_object* l_Lean_Level_quote___main___closed__6;
 lean_object* l_Lean_Delaborator_mkDelabAttribute___lambda__1___closed__2;
 lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabSort___closed__7;
-extern lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___closed__5;
 lean_object* l_Lean_Delaborator_annotateCurPos(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Delaborator_delabAppExplicit___closed__3;
 extern lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__1;
@@ -464,6 +462,7 @@ extern lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__4;
 lean_object* l_Lean_Delaborator_getImplicitParams___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_usize_to_nat(size_t);
 lean_object* l_Lean_Delaborator_withAppFnArgs___main(lean_object*);
+extern lean_object* l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__5;
 uint8_t l_Lean_getPPAll(lean_object*);
 lean_object* l_Lean_Delaborator_getExprKind___closed__3;
 lean_object* l_Lean_Delaborator_delabOfNat___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -479,6 +478,7 @@ lean_object* l_Lean_getPPStructureProjections___closed__2;
 lean_object* l_Lean_Level_quote(lean_object*);
 lean_object* l_Array_findIdxAux___main___at_Lean_Delaborator_annotatePos___main___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l___private_Lean_Delaborator_2__delabBinders___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_Term_namedPattern_x27___elambda__1___closed__5;
 lean_object* l_Lean_Delaborator_delabConst___closed__3;
 lean_object* l___regBuiltin_Lean_Delaborator_delabForall(lean_object*);
 lean_object* l_Array_anyRangeMAux___main___at_Lean_Delaborator_hasIdent___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -8563,7 +8563,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_SourceInfo_inhabited___closed__1;
-x_2 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__5;
+x_2 = l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__5;
 x_3 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -9379,7 +9379,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_SourceInfo_inhabited___closed__1;
-x_2 = l_Lean_Parser_Term_namedPattern___elambda__1___closed__5;
+x_2 = l_Lean_Parser_Term_namedPattern_x27___elambda__1___closed__5;
 x_3 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);

stage0/stdlib/Lean/Elab/Binders.c

@@ -205,11 +205,11 @@ lean_object* l_Lean_Elab_Term_mkFreshInstanceName___rarg(lean_object*);
 extern lean_object* l_Lean_formatEntry___closed__1;
 lean_object* l_Lean_Elab_Term_isClass(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-uint8_t l_Lean_Elab_Term_Quotation_isAntiquot(lean_object*);
 lean_object* l_Lean_mkFVar(lean_object*);
 extern lean_object* l_Lean_Expr_getAutoParamTactic_x3f___closed__1;
 lean_object* l_Lean_Elab_Term_quoteAutoTactic(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
+uint8_t l_Lean_Syntax_isAntiquot(lean_object*);
 uint8_t l_Lean_Expr_isAutoParam(lean_object*);
 extern lean_object* l_Lean_Expr_getAutoParamTactic_x3f___closed__2;
 extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10;
@@ -881,7 +881,7 @@ x_7 = lean_ctor_get(x_1, 0);
 lean_inc(x_7);
 x_8 = lean_ctor_get(x_1, 1);
 lean_inc(x_8);
-x_9 = l_Lean_Elab_Term_Quotation_isAntiquot(x_1);
+x_9 = l_Lean_Syntax_isAntiquot(x_1);
 if (x_9 == 0)
 {
 uint8_t x_10; 

stage0/stdlib/Lean/Elab/Print.c

@@ -38,7 +38,6 @@ lean_object* l_IO_Prim_Ref_set___boxed(lean_object*, lean_object*, lean_object*,
 lean_object* l___private_Lean_Elab_Command_3__mkTermContext(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Print_6__printQuot___rarg___closed__1;
 extern lean_object* l_Lean_Parser_Command_print___elambda__1___closed__2;
-extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__5;
 lean_object* l_List_map___main___at___private_Lean_Elab_Print_9__printId___spec__2(lean_object*);
 lean_object* l_Lean_Elab_Command_elabPrint___closed__4;
 extern lean_object* l_Lean_Meta_Exception_Inhabited___closed__1;
@@ -102,6 +101,7 @@ lean_object* l___private_Lean_Elab_Print_7__printInduct___boxed(lean_object*, le
 lean_object* l___private_Lean_Elab_Print_7__printInduct___closed__1;
 uint8_t l_List_isEmpty___rarg(lean_object*);
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__5;
 lean_object* l___private_Lean_Elab_Print_2__lparamsToMessageData___closed__3;
 lean_object* l___private_Lean_Elab_Print_8__printIdCore___closed__2;
 lean_object* l___private_Lean_Elab_Print_6__printQuot___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -165,7 +165,7 @@ lean_object* _init_l___private_Lean_Elab_Print_2__lparamsToMessageData___closed_
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__5;
+x_1 = l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__5;
 x_2 = lean_alloc_ctor(2, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;

stage0/stdlib/Lean/Elab/Quotation.c

@@ -14,6 +14,7 @@
 extern "C" {
 #endif
 lean_object* l_List_reverse___rarg(lean_object*);
+uint8_t l_Lean_Syntax_isQuot(lean_object*);
 extern lean_object* l_Lean_Expr_eq_x3f___closed__1;
 extern lean_object* l_Lean_mkHole___closed__3;
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__56;
@@ -39,7 +40,6 @@ lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__10;
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__32;
 lean_object* l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__33;
 lean_object* l_Lean_mkTermIdFromIdent(lean_object*);
-uint8_t l_Lean_Elab_Term_Quotation_isQuot(lean_object*);
 extern lean_object* l_Lean_Nat_HasQuote___closed__2;
 lean_object* l_unreachable_x21___rarg(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_10__toPreterm___main___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -107,7 +107,6 @@ lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___close
 lean_object* l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__16;
 lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__2;
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__50;
-extern lean_object* l_Lean_Parser_mkAntiquot___closed__4;
 lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
@@ -160,6 +159,7 @@ extern lean_object* l_Lean_Elab_Term_expandCDot_x3f___closed__4;
 extern lean_object* l_Lean_mkAppStx___closed__7;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__1___closed__5;
+extern lean_object* l_Lean_Parser_mkAntiquot___closed__3;
 lean_object* l___private_Lean_Elab_Quotation_10__toPreterm___main___closed__3;
 lean_object* l_List_filterAux___main___at___private_Lean_Elab_Quotation_6__compileStxMatch___main___spec__4___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__61;
@@ -359,7 +359,6 @@ lean_object* l_ReaderT_bind___at_Lean_Elab_Term_monadLog___spec__2___rarg(lean_o
 lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_quot___elambda__1___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__47;
-uint8_t l_Lean_Elab_Term_Quotation_isAntiquot(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__60;
 lean_object* l_Lean_mkFVar(lean_object*);
 extern lean_object* l_Lean_optionToExpr___rarg___lambda__1___closed__3;
@@ -367,6 +366,7 @@ extern lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_5__explodeHeadPat___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__6;
 extern lean_object* l_Lean_nullKind___closed__1;
+uint8_t l_Lean_Syntax_isAntiquot(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_11__oldRunTermElabM___rarg___closed__4;
 lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__10;
@@ -386,7 +386,6 @@ lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__25;
 extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___lambda__1___closed__5;
 lean_object* l_List_map___main___at___private_Lean_Elab_Quotation_11__oldRunTermElabM___spec__2(lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_termElabAttribute;
-lean_object* l_Lean_Elab_Term_Quotation_isQuot___boxed(lean_object*);
 lean_object* l___private_Lean_Elab_Quotation_5__explodeHeadPat___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_letDecl___closed__1;
 extern lean_object* l_Lean_mkAppStx___closed__3;
@@ -470,7 +469,6 @@ lean_object* l_List_mapM___main___at___private_Lean_Elab_Quotation_6__compileStx
 extern lean_object* l___private_Lean_Meta_LevelDefEq_10__processPostponedStep___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_1__elimAntiquotChoices(lean_object*);
 lean_object* l_Lean_Elab_Term_adaptExpander(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_Quotation_isAntiquot___boxed(lean_object*);
 lean_object* l_Lean_mkStxStrLit(lean_object*, lean_object*);
 uint8_t l_Lean_Elab_Term_Quotation_isAntiquotSplice(lean_object*);
 lean_object* lean_parse_expr(lean_object*, lean_object*, lean_object*);
@@ -529,6 +527,7 @@ extern lean_object* l_Lean_MetavarContext_Inhabited___closed__1;
 extern lean_object* l_Lean_mkOptionalNode___closed__2;
 lean_object* l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_11__oldRunTermElabM(lean_object*);
+extern lean_object* l_Lean_Syntax_isAntiquot___closed__1;
 extern lean_object* l_Lean_Unhygienic_run___rarg___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_10__toPreterm___main___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkNatLit(lean_object*);
@@ -565,7 +564,6 @@ lean_object* l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed_
 lean_object* l___private_Lean_Elab_Quotation_1__elimAntiquotChoices___main(lean_object*);
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Quotation_elabLevelQuot(lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__4;
 lean_object* l___private_Lean_Elab_Quotation_10__toPreterm___main___lambda__2___closed__4;
 extern lean_object* l_Lean_Parser_Term_and___elambda__1___closed__1;
 lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__43;
@@ -598,87 +596,6 @@ lean_object* l_monadInhabited___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_replaceRef(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_Quotation_elabMatchSyntax___closed__1;
 uint8_t l_Lean_Syntax_isIdent(lean_object*);
-extern lean_object* l_Lean_Parser_mkAntiquot___closed__1;
-uint8_t l_Lean_Elab_Term_Quotation_isQuot(lean_object* x_1) {
-_start:
-{
-if (lean_obj_tag(x_1) == 1)
-{
-lean_object* x_2; 
-x_2 = lean_ctor_get(x_1, 0);
-if (lean_obj_tag(x_2) == 1)
-{
-lean_object* x_3; lean_object* x_4; uint8_t x_5; 
-x_3 = lean_ctor_get(x_2, 1);
-x_4 = l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__3;
-x_5 = lean_string_dec_eq(x_3, x_4);
-return x_5;
-}
-else
-{
-uint8_t x_6; 
-x_6 = 0;
-return x_6;
-}
-}
-else
-{
-uint8_t x_7; 
-x_7 = 0;
-return x_7;
-}
-}
-}
-lean_object* l_Lean_Elab_Term_Quotation_isQuot___boxed(lean_object* x_1) {
-_start:
-{
-uint8_t x_2; lean_object* x_3; 
-x_2 = l_Lean_Elab_Term_Quotation_isQuot(x_1);
-lean_dec(x_1);
-x_3 = lean_box(x_2);
-return x_3;
-}
-}
-uint8_t l_Lean_Elab_Term_Quotation_isAntiquot(lean_object* x_1) {
-_start:
-{
-if (lean_obj_tag(x_1) == 1)
-{
-lean_object* x_2; 
-x_2 = lean_ctor_get(x_1, 0);
-if (lean_obj_tag(x_2) == 1)
-{
-lean_object* x_3; lean_object* x_4; uint8_t x_5; 
-x_3 = lean_ctor_get(x_2, 1);
-x_4 = l_Lean_Parser_mkAntiquot___closed__1;
-x_5 = lean_string_dec_eq(x_3, x_4);
-return x_5;
-}
-else
-{
-uint8_t x_6; 
-x_6 = 0;
-return x_6;
-}
-}
-else
-{
-uint8_t x_7; 
-x_7 = 0;
-return x_7;
-}
-}
-}
-lean_object* l_Lean_Elab_Term_Quotation_isAntiquot___boxed(lean_object* x_1) {
-_start:
-{
-uint8_t x_2; lean_object* x_3; 
-x_2 = l_Lean_Elab_Term_Quotation_isAntiquot(x_1);
-lean_dec(x_1);
-x_3 = lean_box(x_2);
-return x_3;
-}
-}
 uint8_t l_Lean_Elab_Term_Quotation_isEscapedAntiquot(lean_object* x_1) {
 _start:
 {
@@ -717,7 +634,7 @@ lean_object* l_Lean_Elab_Term_Quotation_unescapeAntiquot(lean_object* x_1) {
 _start:
 {
 uint8_t x_2; 
-x_2 = l_Lean_Elab_Term_Quotation_isAntiquot(x_1);
+x_2 = l_Lean_Syntax_isAntiquot(x_1);
 if (x_2 == 0)
 {
 return x_1;
@@ -794,7 +711,7 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t
 x_3 = lean_ctor_get(x_1, 1);
 x_4 = lean_ctor_get(x_2, 0);
 x_5 = lean_ctor_get(x_2, 1);
-x_6 = l_Lean_Parser_mkAntiquot___closed__1;
+x_6 = l_Lean_Syntax_isAntiquot___closed__1;
 x_7 = lean_string_dec_eq(x_5, x_6);
 if (x_7 == 0)
 {
@@ -808,7 +725,7 @@ lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8
 x_9 = l_Lean_Syntax_inhabited;
 x_10 = lean_unsigned_to_nat(3u);
 x_11 = lean_array_get(x_9, x_3, x_10);
-x_12 = l_Lean_Parser_mkAntiquot___closed__4;
+x_12 = l_Lean_Parser_mkAntiquot___closed__3;
 x_13 = l_Lean_Syntax_isOfKind(x_11, x_12);
 if (x_13 == 0)
 {
@@ -854,7 +771,7 @@ uint8_t l_Lean_Elab_Term_Quotation_isAntiquotSplice(lean_object* x_1) {
 _start:
 {
 uint8_t x_2; 
-x_2 = l_Lean_Elab_Term_Quotation_isAntiquot(x_1);
+x_2 = l_Lean_Syntax_isAntiquot(x_1);
 if (x_2 == 0)
 {
 uint8_t x_3; 
@@ -2306,7 +2223,7 @@ case 1:
 lean_object* x_7; lean_object* x_8; uint8_t x_114; 
 x_7 = lean_ctor_get(x_1, 0);
 lean_inc(x_7);
-x_114 = l_Lean_Elab_Term_Quotation_isAntiquot(x_1);
+x_114 = l_Lean_Syntax_isAntiquot(x_1);
 if (x_114 == 0)
 {
 lean_object* x_115; 
@@ -4468,7 +4385,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Elab_Term_termElabAttribute;
-x_3 = l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__4;
+x_3 = l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__3;
 x_4 = l___regBuiltin_Lean_Elab_Term_Quotation_elabfunBinderQuot___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
@@ -5531,7 +5448,7 @@ x_7 = l_Lean_Syntax_isOfKind(x_3, x_6);
 if (x_7 == 0)
 {
 uint8_t x_8; 
-x_8 = l_Lean_Elab_Term_Quotation_isQuot(x_3);
+x_8 = l_Lean_Syntax_isQuot(x_3);
 if (x_8 == 0)
 {
 lean_object* x_9; lean_object* x_10; lean_object* x_11; 
@@ -5553,7 +5470,7 @@ x_50 = l_Lean_Syntax_isAtom(x_13);
 if (x_50 == 0)
 {
 uint8_t x_51; 
-x_51 = l_Lean_Elab_Term_Quotation_isAntiquot(x_13);
+x_51 = l_Lean_Syntax_isAntiquot(x_13);
 if (x_51 == 0)
 {
 lean_object* x_52; 
@@ -10865,7 +10782,7 @@ if (lean_obj_tag(x_1) == 1)
 {
 lean_object* x_2; uint8_t x_3; 
 x_2 = lean_ctor_get(x_1, 1);
-x_3 = l_Lean_Elab_Term_Quotation_isAntiquot(x_1);
+x_3 = l_Lean_Syntax_isAntiquot(x_1);
 if (x_3 == 0)
 {
 lean_object* x_4; lean_object* x_5; lean_object* x_6; 
@@ -10950,7 +10867,7 @@ lean_object* l_Lean_Elab_Term_Quotation_getPatternVars(lean_object* x_1) {
 _start:
 {
 uint8_t x_2; 
-x_2 = l_Lean_Elab_Term_Quotation_isQuot(x_1);
+x_2 = l_Lean_Syntax_isQuot(x_1);
 if (x_2 == 0)
 {
 lean_object* x_3; uint8_t x_4; 
@@ -13333,7 +13250,7 @@ goto block_57;
 block_57:
 {
 uint8_t x_15; 
-x_15 = l_Lean_Elab_Term_Quotation_isQuot(x_13);
+x_15 = l_Lean_Syntax_isQuot(x_13);
 if (x_15 == 0)
 {
 lean_object* x_16; lean_object* x_17; 

stage0/stdlib/Lean/Elab/Syntax.c

@@ -15,6 +15,7 @@ extern "C" {
 #endif
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__45;
 lean_object* l_List_reverse___rarg(lean_object*);
+uint8_t l_Lean_Syntax_isQuot(lean_object*);
 lean_object* l_Lean_Elab_Command_elabSyntax___closed__11;
 lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__34;
 lean_object* l_Lean_Elab_Command_expandElab___closed__43;
@@ -57,7 +58,6 @@ lean_object* l_Lean_Elab_Command_elabSyntaxAbbrev___lambda__1___boxed(lean_objec
 extern lean_object* l_Lean_Parser_Syntax_many1___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Command_expandMacroArgIntoSyntaxItem(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Command_elabReserve___closed__1;
-uint8_t l_Lean_Elab_Term_Quotation_isQuot(lean_object*);
 extern lean_object* l_Lean_Nat_HasQuote___closed__2;
 lean_object* l_unreachable_x21___rarg(lean_object*);
 lean_object* l_Lean_Elab_Command_elabMacroRulesAux___lambda__1___closed__4;
@@ -464,7 +464,6 @@ lean_object* l_Lean_Elab_Command_expandElab___closed__13;
 extern lean_object* l_Lean_Elab_Term_mkTermElabAttribute___closed__9;
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__126;
 uint8_t l_Lean_Name_hasMacroScopes___main(lean_object*);
-extern lean_object* l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__3;
 lean_object* l_Lean_Parser_registerParserCategory(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__63;
 extern lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__1___closed__3;
@@ -712,7 +711,7 @@ lean_object* l___private_Lean_Elab_Syntax_1__mkParserSeq___boxed(lean_object*, l
 extern lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Command_expandNotationItemIntoSyntaxItem(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__35;
-extern lean_object* l_Lean_Parser_mkAntiquot___closed__2;
+extern lean_object* l_Lean_Syntax_isQuot___closed__1;
 lean_object* l_Lean_Elab_Command_getOptions___rarg(lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Command_liftTermElabM___rarg___closed__1;
 extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1;
@@ -748,6 +747,7 @@ extern lean_object* l_Lean_Parser_Command_declId___elambda__1___closed__2;
 lean_object* l___private_Lean_Elab_Syntax_6__declareSyntaxCatQuotParser___closed__45;
 lean_object* l_Lean_Elab_Command_expandElab___closed__65;
 lean_object* l_Lean_Elab_Command_expandElab___closed__39;
+extern lean_object* l_Lean_Parser_mkAntiquot___closed__1;
 lean_object* l_Lean_Elab_Command_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_expandOptPrecedence(lean_object* x_1) {
 _start:
@@ -8375,7 +8375,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__3;
+x_2 = l_Lean_Syntax_isQuot___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@@ -12463,7 +12463,7 @@ lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
 x_6 = lean_unsigned_to_nat(0u);
 x_7 = l_Lean_Syntax_getArg(x_2, x_6);
 x_8 = l_Lean_Syntax_getArg(x_7, x_6);
-x_9 = l_Lean_Elab_Term_Quotation_isQuot(x_8);
+x_9 = l_Lean_Syntax_isQuot(x_8);
 if (x_9 == 0)
 {
 lean_object* x_10; lean_object* x_11; 
@@ -13542,7 +13542,7 @@ x_5 = lean_unsigned_to_nat(0u);
 x_6 = l_Lean_Syntax_getArg(x_1, x_5);
 x_7 = l_Lean_Syntax_getArg(x_6, x_5);
 lean_dec(x_6);
-x_8 = l_Lean_Elab_Term_Quotation_isQuot(x_7);
+x_8 = l_Lean_Syntax_isQuot(x_7);
 if (x_8 == 0)
 {
 lean_object* x_9; lean_object* x_10; 
@@ -15190,7 +15190,7 @@ x_48 = lean_array_push(x_47, x_18);
 x_49 = l_Lean_mkOptionalNode___closed__1;
 x_50 = lean_array_push(x_48, x_49);
 x_51 = lean_array_push(x_50, x_49);
-x_52 = l_Lean_Parser_mkAntiquot___closed__2;
+x_52 = l_Lean_Parser_mkAntiquot___closed__1;
 x_53 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_53, 0, x_52);
 lean_ctor_set(x_53, 1, x_51);
@@ -15503,7 +15503,7 @@ x_20 = lean_array_push(x_19, x_18);
 x_21 = l_Lean_mkOptionalNode___closed__1;
 x_22 = lean_array_push(x_20, x_21);
 x_23 = lean_array_push(x_22, x_21);
-x_24 = l_Lean_Parser_mkAntiquot___closed__2;
+x_24 = l_Lean_Parser_mkAntiquot___closed__1;
 x_25 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_25, 0, x_24);
 lean_ctor_set(x_25, 1, x_23);
@@ -16690,7 +16690,7 @@ x_15 = lean_array_push(x_14, x_13);
 x_16 = l_Lean_mkOptionalNode___closed__1;
 x_17 = lean_array_push(x_15, x_16);
 x_18 = lean_array_push(x_17, x_16);
-x_19 = l_Lean_Parser_mkAntiquot___closed__2;
+x_19 = l_Lean_Parser_mkAntiquot___closed__1;
 x_20 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_20, 0, x_19);
 lean_ctor_set(x_20, 1, x_18);
@@ -17798,7 +17798,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Elab_Command_expandElab___closed__16;
-x_2 = l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__3;
+x_2 = l_Lean_Syntax_isQuot___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }

stage0/stdlib/Lean/Parser/Tactic.c

@@ -31,6 +31,7 @@ lean_object* l_Lean_Parser_Tactic_exact___closed__6;
 lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Tactic_orelse___closed__2;
 lean_object* l_Lean_Parser_Tactic_intros___closed__7;
+lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__10;
 lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Tactic_induction___closed__1;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__1;
@@ -113,7 +114,6 @@ lean_object* l_Lean_Parser_Tactic_withAlts___closed__1;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Tactic_subst_parenthesizer___closed__1;
 lean_object* l___regBuiltin_Lean_Parser_Tactic_case_parenthesizer(lean_object*);
-extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Tactic_clear___closed__6;
 lean_object* l_Lean_Parser_Tactic_allGoals_parenthesizer___closed__3;
 lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__6;
@@ -154,6 +154,7 @@ lean_object* l_Lean_Parser_Tactic_clear___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Tactic_usingRec___closed__1;
 lean_object* l_Lean_Parser_Tactic_orelse___closed__7;
 lean_object* l_Lean_Parser_Tactic_injection_parenthesizer___closed__4;
+extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Tactic_underscore;
 lean_object* l_Lean_Parser_Tactic_traceState___elambda__1___closed__4;
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
@@ -207,7 +208,6 @@ lean_object* l_Lean_Parser_Tactic_assumption_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Tactic_generalize___closed__3;
 lean_object* l_Lean_Parser_Tactic_orelse___closed__5;
 lean_object* l_Lean_Parser_Tactic_withIds;
-extern lean_object* l_Lean_Parser_Term_optIdent___closed__2;
 lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Tactic_revert___closed__4;
 lean_object* l_Lean_Parser_Tactic_majorPremise_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -270,10 +270,10 @@ lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser
 lean_object* l_Lean_Parser_Tactic_generalizingVars___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Tactic_usingRec___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__7;
-extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_inductionAlts___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_traceState___closed__5;
 lean_object* l___regBuiltin_Lean_Parser_Tactic_injection_parenthesizer___closed__1;
+lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__8;
 lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__10;
 lean_object* l_Lean_Parser_Tactic_inductionAlt_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -344,6 +344,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_allGoals_parenthesizer(lean_objec
 lean_object* l_Lean_Parser_Tactic_ident_x27___closed__1;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_revert(lean_object*);
 lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__9;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_intros(lean_object*);
 lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__6;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_visitArgs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -358,6 +359,7 @@ lean_object* l_Lean_Parser_Tactic_intros___closed__2;
 lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__12;
 lean_object* l___regBuiltin_Lean_Parser_Tactic_nestedTacticBlock_parenthesizer(lean_object*);
 uint8_t l_Lean_Parser_tryAnti(lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_Level_ident_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__7;
 lean_object* l_Lean_Parser_optionaInfo(lean_object*);
 lean_object* l_Lean_Parser_Tactic_cases___closed__2;
@@ -370,6 +372,7 @@ lean_object* l_Lean_Parser_Tactic_revert___closed__5;
 lean_object* l_Lean_Parser_Tactic_traceState___closed__4;
 lean_object* l___regBuiltin_Lean_Parser_Tactic_intro_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Tactic_skip___closed__5;
+extern lean_object* l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__11;
 lean_object* l_Lean_Parser_Tactic_withIds___closed__4;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_apply(lean_object*);
 lean_object* l_Lean_Parser_Tactic_cases___elambda__1___closed__2;
@@ -389,6 +392,7 @@ lean_object* l_Lean_Parser_Tactic_intro_parenthesizer___closed__5;
 lean_object* l_Lean_Parser_Tactic_inductionAlts___closed__5;
 extern lean_object* l_Lean_Parser_Term_namedHole;
 lean_object* l_Lean_Parser_Tactic_allGoals_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__5;
 extern lean_object* l_Char_HasRepr___closed__1;
 lean_object* l___regBuiltin_Lean_Parser_Tactic_cases_parenthesizer(lean_object*);
 lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__7;
@@ -418,11 +422,11 @@ lean_object* l_Lean_Parser_Tactic_paren_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Tactic_exact___closed__3;
 lean_object* l_Lean_Parser_Tactic_inductionAlts___closed__3;
 lean_object* l_Lean_Parser_Tactic_paren___closed__5;
-extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__10;
 lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Tactic_traceState___closed__6;
 lean_object* l___regBuiltin_Lean_Parser_Tactic_skip_parenthesizer(lean_object*);
 lean_object* l___regBuiltin_Lean_Parser_Tactic_clear_parenthesizer___closed__1;
+lean_object* l_Lean_Parser_Tactic_generalize___closed__13;
 lean_object* l_Lean_Parser_Tactic_assumption___closed__2;
 lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__8;
 extern lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__11;
@@ -459,7 +463,6 @@ extern lean_object* l_Lean_Parser_Term_structInst___closed__2;
 lean_object* l_Lean_Parser_Tactic_inductionAlt_parenthesizer___closed__5;
 lean_object* l_Lean_Parser_Tactic_orelse_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock;
-extern lean_object* l_Lean_Parser_Term_explicitUniv___closed__4;
 lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__3;
@@ -492,7 +495,6 @@ lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_
 lean_object* l_Lean_Parser_Tactic_failIfSuccess;
 lean_object* l_Lean_Parser_Tactic_paren___closed__1;
 lean_object* l___regBuiltin_Lean_Parser_Tactic_assumption_parenthesizer___closed__1;
-extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__3;
 lean_object* l_Lean_Parser_Tactic_generalize___closed__10;
 lean_object* l_Lean_Parser_Tactic_paren___closed__2;
 lean_object* l_Lean_Parser_Tactic_subst___closed__3;
@@ -516,14 +518,12 @@ lean_object* l_Lean_Parser_Tactic_failIfSuccess_parenthesizer(lean_object*, lean
 lean_object* l_Lean_Parser_Tactic_orelse;
 lean_object* l_Lean_Parser_Tactic_allGoals___closed__6;
 lean_object* l_Lean_Parser_Tactic_subst___closed__5;
-extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__5;
 lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_subst;
 lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Tactic_case_parenthesizer___closed__4;
 lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__8;
-extern lean_object* l_Lean_Parser_Level_ident_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Tactic_intros___elambda__1___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_failIfSuccess___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__4;
@@ -606,6 +606,7 @@ lean_object* l_Lean_Parser_Tactic_generalizingVars;
 lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__9;
 lean_object* l_Lean_Parser_Tactic_induction___closed__3;
 lean_object* l_Lean_Parser_symbolInfo(lean_object*);
+extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__11;
 lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_induction_parenthesizer___closed__10;
 lean_object* l_Lean_Parser_Tactic_revert___elambda__1___closed__5;
@@ -621,7 +622,7 @@ lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__4;
 lean_object* l_Lean_Parser_Tactic_assumption___closed__3;
 lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__7;
 lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__2(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11;
+extern lean_object* l_Lean_Parser_Term_typeAscription___closed__1;
 lean_object* l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -672,6 +673,7 @@ lean_object* l_Lean_Parser_Tactic_revert_parenthesizer___closed__3;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_assumption(lean_object*);
 extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__2___closed__6;
 extern lean_object* l_Lean_Parser_Term_implicitBinder___closed__1;
+extern lean_object* l_Lean_Parser_Term_typeAscription___closed__2;
 extern lean_object* l_Lean_Parser_Term_matchAlts___closed__1;
 lean_object* l_Lean_Parser_Tactic_underscoreFn___closed__2;
 lean_object* l_Lean_Parser_Tactic_induction_parenthesizer___closed__9;
@@ -712,7 +714,6 @@ lean_object* l___regBuiltinParser_Lean_Parser_Tactic_induction(lean_object*);
 lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Tactic_induction___closed__9;
 lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__3;
-extern lean_object* l_Lean_Parser_Term_optIdent_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Tactic_allGoals___closed__4;
 lean_object* l_Lean_Parser_Tactic_revert___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Tactic_clear___closed__7;
@@ -724,7 +725,6 @@ lean_object* l_Lean_Parser_Tactic_generalizingVars___closed__3;
 lean_object* l_Lean_Parser_Tactic_withAlts_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Tactic_cases_parenthesizer___closed__3;
-extern lean_object* l_Lean_Parser_Term_namedHole_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Tactic_underscore_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_inductionAlts___closed__1;
 lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7;
@@ -778,6 +778,7 @@ lean_object* l_Lean_Parser_Tactic_intros_parenthesizer(lean_object*, lean_object
 extern lean_object* l_Lean_Parser_Parser_inhabited___closed__1;
 lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__3(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_refine;
+lean_object* l_Lean_Parser_Tactic_generalize___closed__14;
 extern lean_object* l_Lean_Parser_Tactic_nonEmptySeq_parenthesizer___closed__1;
 extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Tactic_generalize___closed__5;
@@ -799,6 +800,7 @@ lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__6;
 lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Tactic_traceState___elambda__1(lean_object*, lean_object*);
+lean_object* l_Lean_PrettyPrinter_Parenthesizer_try_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_paren___closed__7;
 extern lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__14;
 lean_object* l_Lean_Parser_Tactic_clear_parenthesizer___closed__1;
@@ -810,6 +812,8 @@ lean_object* l_Lean_Parser_Tactic_majorPremise;
 lean_object* l_Lean_Parser_Tactic_failIfSuccess___elambda__1___closed__5;
 lean_object* l___regBuiltinParser_Lean_Parser_Tactic_injection(lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_Term_explicitUniv_x27___closed__4;
+extern lean_object* l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__7;
 lean_object* l_Lean_Parser_andthenFn(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* _init_l_Lean_Parser_Tactic_underscoreFn___closed__1() {
 _start:
@@ -1509,7 +1513,7 @@ lean_object* l_Lean_Parser_Tactic_ident_x27_parenthesizer(lean_object* x_1, lean
 _start:
 {
 lean_object* x_5; lean_object* x_6; lean_object* x_7; 
-x_5 = l_Lean_Parser_Level_ident_parenthesizer___closed__2;
+x_5 = l_Lean_Parser_Level_ident_parenthesizer___closed__1;
 x_6 = l_Lean_Parser_Tactic_ident_x27_parenthesizer___closed__1;
 x_7 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_5, x_6, x_1, x_2, x_3, x_4);
 return x_7;
@@ -2539,7 +2543,7 @@ lean_object* _init_l_Lean_Parser_Tactic_revert_parenthesizer___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Level_ident_parenthesizer___closed__2;
+x_1 = l_Lean_Parser_Level_ident_parenthesizer___closed__1;
 x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_many1_parenthesizer), 5, 1);
 lean_closure_set(x_2, 0, x_1);
 return x_2;
@@ -4024,7 +4028,7 @@ lean_object* _init_l_Lean_Parser_Tactic_apply___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2;
+x_1 = l_Lean_Parser_Term_typeAscription___closed__2;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
 x_3 = l_Lean_Parser_Tactic_apply___closed__1;
@@ -4419,7 +4423,7 @@ lean_object* _init_l_Lean_Parser_Tactic_exact___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2;
+x_1 = l_Lean_Parser_Term_typeAscription___closed__2;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
 x_3 = l_Lean_Parser_Tactic_exact___closed__1;
@@ -4802,7 +4806,7 @@ lean_object* _init_l_Lean_Parser_Tactic_refine___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2;
+x_1 = l_Lean_Parser_Term_typeAscription___closed__2;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
 x_3 = l_Lean_Parser_Tactic_refine___closed__1;
@@ -5322,7 +5326,7 @@ lean_object* _init_l_Lean_Parser_Tactic_case_parenthesizer___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Level_ident_parenthesizer___closed__2;
+x_1 = l_Lean_Parser_Level_ident_parenthesizer___closed__1;
 x_2 = l_Lean_Parser_Tactic_nonEmptySeq_parenthesizer___closed__1;
 x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
 lean_closure_set(x_3, 0, x_1);
@@ -7694,6 +7698,27 @@ return x_3;
 lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__2() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_ident;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Term_typeAscription___closed__1;
+x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Tactic_generalize___closed__2;
+x_2 = l_Lean_Parser_optionaInfo(x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__4() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_termParser___closed__2;
 x_2 = lean_unsigned_to_nat(51u);
@@ -7701,7 +7726,7 @@ x_3 = l_Lean_Parser_categoryParser(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__3() {
+lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
@@ -7710,57 +7735,37 @@ x_2 = l_Lean_Parser_symbolInfo(x_1);
 return x_2;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__4() {
+lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_ident;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Tactic_generalize___closed__3;
+x_3 = l_Lean_Parser_Tactic_generalize___closed__5;
 x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
 return x_4;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__5() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_Tactic_generalize___closed__2;
-x_2 = lean_ctor_get(x_1, 0);
-lean_inc(x_2);
-x_3 = l_Lean_Parser_Tactic_generalize___closed__4;
-x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
-return x_4;
-}
-}
-lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__6() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_optIdent___closed__2;
-x_2 = l_Lean_Parser_Tactic_generalize___closed__5;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
 lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__7() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_generalize___closed__1;
-x_2 = l_Lean_Parser_Tactic_generalize___closed__6;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_Tactic_generalize___closed__4;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Tactic_generalize___closed__6;
+x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
+return x_4;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__8() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2;
+x_1 = l_Lean_Parser_Tactic_generalize___closed__3;
 x_2 = l_Lean_Parser_Tactic_generalize___closed__7;
-x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
 return x_3;
 }
 }
@@ -7768,7 +7773,7 @@ lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_epsilonInfo;
+x_1 = l_Lean_Parser_Tactic_generalize___closed__1;
 x_2 = l_Lean_Parser_Tactic_generalize___closed__8;
 x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
 return x_3;
@@ -7777,16 +7782,36 @@ return x_3;
 lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__10() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2;
+x_2 = l_Lean_Parser_Tactic_generalize___closed__9;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__11() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_epsilonInfo;
+x_2 = l_Lean_Parser_Tactic_generalize___closed__10;
+x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__12() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__4;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Tactic_generalize___closed__9;
+x_3 = l_Lean_Parser_Tactic_generalize___closed__11;
 x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
 return x_4;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__11() {
+lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__13() {
 _start:
 {
 lean_object* x_1; 
@@ -7794,12 +7819,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_generalize___elambda__1),
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__12() {
+lean_object* _init_l_Lean_Parser_Tactic_generalize___closed__14() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_generalize___closed__10;
-x_2 = l_Lean_Parser_Tactic_generalize___closed__11;
+x_1 = l_Lean_Parser_Tactic_generalize___closed__12;
+x_2 = l_Lean_Parser_Tactic_generalize___closed__13;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -7810,7 +7835,7 @@ lean_object* _init_l_Lean_Parser_Tactic_generalize() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Tactic_generalize___closed__12;
+x_1 = l_Lean_Parser_Tactic_generalize___closed__14;
 return x_1;
 }
 }
@@ -7842,14 +7867,36 @@ return x_4;
 lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Level_ident_parenthesizer___closed__1;
+x_2 = l_Lean_PrettyPrinter_Parenthesizer_compileParenthesizerDescr___main___closed__1;
+x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
+lean_closure_set(x_3, 0, x_1);
+lean_closure_set(x_3, 1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Term_optIdent_parenthesizer___closed__2;
+x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2;
+x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_try_parenthesizer), 5, 1);
+lean_closure_set(x_2, 0, x_1);
+return x_2;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3;
 x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_optional_parenthesizer), 5, 1);
 lean_closure_set(x_2, 0, x_1);
 return x_2;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3() {
+lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
@@ -7859,36 +7906,12 @@ lean_closure_set(x_2, 0, x_1);
 return x_2;
 }
 }
-lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__4() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3;
-x_2 = l_Lean_Parser_Term_namedHole_parenthesizer___closed__2;
-x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
-lean_closure_set(x_3, 0, x_1);
-lean_closure_set(x_3, 1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__5() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2;
-x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__4;
-x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
-lean_closure_set(x_3, 0, x_1);
-lean_closure_set(x_3, 1, x_2);
-return x_3;
-}
-}
 lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_PrettyPrinter_Parenthesizer_compileParenthesizerDescr___main___closed__2;
-x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__5;
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_compileParenthesizerDescr___main___closed__1;
+x_2 = l_Lean_Parser_Level_ident_parenthesizer___closed__1;
 x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
@@ -7898,10 +7921,46 @@ return x_3;
 lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__5;
+x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
+x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
+lean_closure_set(x_3, 0, x_1);
+lean_closure_set(x_3, 1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__8() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__4;
+x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7;
+x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
+lean_closure_set(x_3, 0, x_1);
+lean_closure_set(x_3, 1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__9() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_compileParenthesizerDescr___main___closed__2;
+x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__8;
+x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
+lean_closure_set(x_3, 0, x_1);
+lean_closure_set(x_3, 1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__10() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2;
 x_2 = lean_unsigned_to_nat(1024u);
-x_3 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
+x_3 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__9;
 x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer), 7, 3);
 lean_closure_set(x_4, 0, x_1);
 lean_closure_set(x_4, 1, x_2);
@@ -7914,7 +7973,7 @@ _start:
 {
 lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_5 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__1;
-x_6 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7;
+x_6 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__10;
 x_7 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_5, x_6, x_1, x_2, x_3, x_4);
 return x_7;
 }
@@ -8586,10 +8645,10 @@ lean_object* _init_l_Lean_Parser_Tactic_majorPremise___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2;
+x_1 = l_Lean_Parser_Term_typeAscription___closed__2;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Term_optIdent___closed__2;
+x_3 = l_Lean_Parser_Tactic_generalize___closed__3;
 x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
 return x_4;
 }
@@ -12047,7 +12106,7 @@ lean_object* _init_l_Lean_Parser_Tactic_majorPremise_parenthesizer___closed__2()
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2;
+x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__4;
 x_2 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__1;
 x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
 lean_closure_set(x_3, 0, x_1);
@@ -12083,7 +12142,7 @@ lean_object* l_Lean_Parser_Tactic_usingRec_parenthesizer(lean_object* x_1, lean_
 _start:
 {
 lean_object* x_5; lean_object* x_6; 
-x_5 = l_Lean_Parser_Term_namedHole_parenthesizer___closed__2;
+x_5 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
 x_6 = l_Lean_PrettyPrinter_Parenthesizer_visitArgs(x_5, x_1, x_2, x_3, x_4);
 return x_6;
 }
@@ -13374,7 +13433,7 @@ lean_object* _init_l_Lean_Parser_Tactic_injection___closed__2() {
 _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_Parser_antiquotNestedExpr___closed__2;
+x_1 = l_Lean_Parser_Term_typeAscription___closed__2;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
 x_3 = l_Lean_Parser_Tactic_withIds;
@@ -13656,7 +13715,7 @@ lean_dec(x_47);
 if (x_49 == 0)
 {
 lean_object* x_50; lean_object* x_51; 
-x_50 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__10;
+x_50 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__11;
 x_51 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_50, x_42);
 x_11 = x_51;
 goto block_41;
@@ -13672,7 +13731,7 @@ else
 {
 lean_object* x_52; lean_object* x_53; 
 lean_dec(x_46);
-x_52 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__10;
+x_52 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__11;
 x_53 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_52, x_42);
 x_11 = x_53;
 goto block_41;
@@ -13682,7 +13741,7 @@ else
 {
 lean_object* x_54; lean_object* x_55; 
 lean_dec(x_44);
-x_54 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__10;
+x_54 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__11;
 x_55 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_54, x_42);
 x_11 = x_55;
 goto block_41;
@@ -13720,13 +13779,13 @@ lean_object* x_20; lean_object* x_21; uint8_t x_22;
 x_20 = lean_ctor_get(x_19, 1);
 lean_inc(x_20);
 lean_dec(x_19);
-x_21 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__4;
+x_21 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__5;
 x_22 = lean_string_dec_eq(x_20, x_21);
 lean_dec(x_20);
 if (x_22 == 0)
 {
 lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
-x_23 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__7;
+x_23 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__8;
 x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_23, x_15);
 x_25 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
 x_26 = l_Lean_Parser_ParserState_mkNode(x_24, x_25, x_10);
@@ -13745,7 +13804,7 @@ else
 {
 lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; 
 lean_dec(x_19);
-x_29 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__7;
+x_29 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__8;
 x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_29, x_15);
 x_31 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
 x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_10);
@@ -13756,7 +13815,7 @@ else
 {
 lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; 
 lean_dec(x_17);
-x_33 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__7;
+x_33 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__8;
 x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_33, x_15);
 x_35 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
 x_36 = l_Lean_Parser_ParserState_mkNode(x_34, x_35, x_10);
@@ -13871,7 +13930,7 @@ lean_dec(x_112);
 if (x_114 == 0)
 {
 lean_object* x_115; lean_object* x_116; 
-x_115 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__10;
+x_115 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__11;
 x_116 = l_Lean_Parser_ParserState_mkErrorsAt(x_108, x_115, x_107);
 x_70 = x_116;
 goto block_106;
@@ -13887,7 +13946,7 @@ else
 {
 lean_object* x_117; lean_object* x_118; 
 lean_dec(x_111);
-x_117 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__10;
+x_117 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__11;
 x_118 = l_Lean_Parser_ParserState_mkErrorsAt(x_108, x_117, x_107);
 x_70 = x_118;
 goto block_106;
@@ -13897,7 +13956,7 @@ else
 {
 lean_object* x_119; lean_object* x_120; 
 lean_dec(x_109);
-x_119 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__10;
+x_119 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__11;
 x_120 = l_Lean_Parser_ParserState_mkErrorsAt(x_108, x_119, x_107);
 x_70 = x_120;
 goto block_106;
@@ -13935,13 +13994,13 @@ lean_object* x_79; lean_object* x_80; uint8_t x_81;
 x_79 = lean_ctor_get(x_78, 1);
 lean_inc(x_79);
 lean_dec(x_78);
-x_80 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__4;
+x_80 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__5;
 x_81 = lean_string_dec_eq(x_79, x_80);
 lean_dec(x_79);
 if (x_81 == 0)
 {
 lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; 
-x_82 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__7;
+x_82 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__8;
 x_83 = l_Lean_Parser_ParserState_mkErrorsAt(x_75, x_82, x_74);
 x_84 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
 x_85 = l_Lean_Parser_ParserState_mkNode(x_83, x_84, x_69);
@@ -13964,7 +14023,7 @@ else
 {
 lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; 
 lean_dec(x_78);
-x_90 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__7;
+x_90 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__8;
 x_91 = l_Lean_Parser_ParserState_mkErrorsAt(x_75, x_90, x_74);
 x_92 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
 x_93 = l_Lean_Parser_ParserState_mkNode(x_91, x_92, x_69);
@@ -13977,7 +14036,7 @@ else
 {
 lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; 
 lean_dec(x_76);
-x_95 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__7;
+x_95 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__8;
 x_96 = l_Lean_Parser_ParserState_mkErrorsAt(x_75, x_95, x_74);
 x_97 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
 x_98 = l_Lean_Parser_ParserState_mkNode(x_96, x_97, x_69);
@@ -14032,7 +14091,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Tactic_nonEmptySeq;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_antiquotNestedExpr___closed__3;
+x_3 = l_Lean_Parser_antiquotNestedExpr___closed__2;
 x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
 return x_4;
 }
@@ -14938,13 +14997,13 @@ lean_object* x_20; lean_object* x_21; uint8_t x_22;
 x_20 = lean_ctor_get(x_19, 1);
 lean_inc(x_20);
 lean_dec(x_19);
-x_21 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__7;
+x_21 = l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__7;
 x_22 = lean_string_dec_eq(x_20, x_21);
 lean_dec(x_20);
 if (x_22 == 0)
 {
 lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
-x_23 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11;
+x_23 = l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__11;
 x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_23, x_15);
 x_25 = l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__2;
 x_26 = l_Lean_Parser_ParserState_mkNode(x_24, x_25, x_10);
@@ -14963,7 +15022,7 @@ else
 {
 lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; 
 lean_dec(x_19);
-x_29 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11;
+x_29 = l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__11;
 x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_29, x_15);
 x_31 = l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__2;
 x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_10);
@@ -14974,7 +15033,7 @@ else
 {
 lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; 
 lean_dec(x_17);
-x_33 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11;
+x_33 = l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__11;
 x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_33, x_15);
 x_35 = l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__2;
 x_36 = l_Lean_Parser_ParserState_mkNode(x_34, x_35, x_10);
@@ -15153,13 +15212,13 @@ lean_object* x_79; lean_object* x_80; uint8_t x_81;
 x_79 = lean_ctor_get(x_78, 1);
 lean_inc(x_79);
 lean_dec(x_78);
-x_80 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__7;
+x_80 = l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__7;
 x_81 = lean_string_dec_eq(x_79, x_80);
 lean_dec(x_79);
 if (x_81 == 0)
 {
 lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; 
-x_82 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11;
+x_82 = l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__11;
 x_83 = l_Lean_Parser_ParserState_mkErrorsAt(x_75, x_82, x_74);
 x_84 = l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__2;
 x_85 = l_Lean_Parser_ParserState_mkNode(x_83, x_84, x_69);
@@ -15182,7 +15241,7 @@ else
 {
 lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; 
 lean_dec(x_78);
-x_90 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11;
+x_90 = l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__11;
 x_91 = l_Lean_Parser_ParserState_mkErrorsAt(x_75, x_90, x_74);
 x_92 = l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__2;
 x_93 = l_Lean_Parser_ParserState_mkNode(x_91, x_92, x_69);
@@ -15195,7 +15254,7 @@ else
 {
 lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; 
 lean_dec(x_76);
-x_95 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11;
+x_95 = l_Lean_Parser_Term_explicitUniv_x27___elambda__1___closed__11;
 x_96 = l_Lean_Parser_ParserState_mkErrorsAt(x_75, x_95, x_74);
 x_97 = l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__2;
 x_98 = l_Lean_Parser_ParserState_mkNode(x_96, x_97, x_69);
@@ -15250,7 +15309,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Tactic_seq;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Term_explicitUniv___closed__4;
+x_3 = l_Lean_Parser_Term_explicitUniv_x27___closed__4;
 x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
 return x_4;
 }
@@ -16403,6 +16462,10 @@ l_Lean_Parser_Tactic_generalize___closed__11 = _init_l_Lean_Parser_Tactic_genera
 lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__11);
 l_Lean_Parser_Tactic_generalize___closed__12 = _init_l_Lean_Parser_Tactic_generalize___closed__12();
 lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__12);
+l_Lean_Parser_Tactic_generalize___closed__13 = _init_l_Lean_Parser_Tactic_generalize___closed__13();
+lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__13);
+l_Lean_Parser_Tactic_generalize___closed__14 = _init_l_Lean_Parser_Tactic_generalize___closed__14();
+lean_mark_persistent(l_Lean_Parser_Tactic_generalize___closed__14);
 l_Lean_Parser_Tactic_generalize = _init_l_Lean_Parser_Tactic_generalize();
 lean_mark_persistent(l_Lean_Parser_Tactic_generalize);
 res = l___regBuiltinParser_Lean_Parser_Tactic_generalize(lean_io_mk_world());
@@ -16422,6 +16485,12 @@ l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6 = _init_l_Lean_Parser_
 lean_mark_persistent(l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6);
 l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7 = _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7();
 lean_mark_persistent(l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7);
+l_Lean_Parser_Tactic_generalize_parenthesizer___closed__8 = _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__8();
+lean_mark_persistent(l_Lean_Parser_Tactic_generalize_parenthesizer___closed__8);
+l_Lean_Parser_Tactic_generalize_parenthesizer___closed__9 = _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__9();
+lean_mark_persistent(l_Lean_Parser_Tactic_generalize_parenthesizer___closed__9);
+l_Lean_Parser_Tactic_generalize_parenthesizer___closed__10 = _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__10();
+lean_mark_persistent(l_Lean_Parser_Tactic_generalize_parenthesizer___closed__10);
 l___regBuiltin_Lean_Parser_Tactic_generalize_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_generalize_parenthesizer___closed__1();
 lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_generalize_parenthesizer___closed__1);
 res = l___regBuiltin_Lean_Parser_Tactic_generalize_parenthesizer(lean_io_mk_world());

stage0/stdlib/Lean/Syntax.c

@@ -13,6 +13,7 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+uint8_t l_Lean_Syntax_isQuot(lean_object*);
 lean_object* l_Lean_Syntax_reprint___main___closed__1;
 lean_object* l_Lean_Syntax_formatStxAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_beq___main___at_Lean_Syntax_structEq___main___spec__2___boxed(lean_object*, lean_object*);
@@ -206,6 +207,7 @@ lean_object* l_Lean_Syntax_getTailInfo___main___boxed(lean_object*);
 lean_object* l_Lean_Syntax_getAtomVal_x21___closed__3;
 lean_object* l_Lean_Syntax_MonadTraverser_goLeft___rarg___lambda__1(lean_object*);
 lean_object* l_Lean_Syntax_MonadTraverser_goUp(lean_object*, lean_object*);
+uint8_t l_Lean_Syntax_isAntiquot(lean_object*);
 lean_object* l_Lean_Syntax_ifNode___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_asNode___boxed(lean_object*);
 uint8_t l_List_beq___main___at_Lean_Syntax_structEq___main___spec__3(lean_object*, lean_object*);
@@ -308,8 +310,10 @@ lean_object* lean_mk_syntax_str_lit(lean_object*);
 lean_object* l_Lean_mkStxLit(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Syntax_7__quoteName___main___closed__2;
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_isAntiquot___boxed(lean_object*);
 extern lean_object* l_Lean_mkOptionalNode___closed__2;
 extern lean_object* l_Lean_Format_paren___closed__3;
+lean_object* l_Lean_Syntax_isAntiquot___closed__1;
 lean_object* l___private_Lean_Syntax_9__quoteOption___rarg___closed__4;
 lean_object* l___private_Lean_Syntax_1__updateInfo(lean_object*, lean_object*);
 lean_object* l_Lean_mkCTermIdFrom(lean_object*, lean_object*);
@@ -333,8 +337,10 @@ extern lean_object* l_Lean_mkAppStx___closed__2;
 extern lean_object* l_String_Inhabited;
 lean_object* l_Lean_Syntax_Traverser_left(lean_object*);
 lean_object* l___private_Lean_Syntax_9__quoteOption___rarg___closed__1;
+lean_object* l_Lean_Syntax_isQuot___boxed(lean_object*);
 lean_object* l_Lean_Syntax_modifyArgs(lean_object*, lean_object*);
 lean_object* l_Lean_mkNode(lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_isQuot___closed__1;
 lean_object* l_Lean_Syntax_getTailInfo___main(lean_object*);
 lean_object* l_Lean_SyntaxNode_getArg(lean_object*, lean_object*);
 lean_object* l_Lean_Format_joinSep___main___at_Lean_Syntax_formatStxAux___main___spec__2___boxed(lean_object*, lean_object*);
@@ -407,6 +413,102 @@ x_3 = lean_box(x_2);
 return x_3;
 }
 }
+lean_object* _init_l_Lean_Syntax_isQuot___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("quot");
+return x_1;
+}
+}
+uint8_t l_Lean_Syntax_isQuot(lean_object* x_1) {
+_start:
+{
+if (lean_obj_tag(x_1) == 1)
+{
+lean_object* x_2; 
+x_2 = lean_ctor_get(x_1, 0);
+if (lean_obj_tag(x_2) == 1)
+{
+lean_object* x_3; lean_object* x_4; uint8_t x_5; 
+x_3 = lean_ctor_get(x_2, 1);
+x_4 = l_Lean_Syntax_isQuot___closed__1;
+x_5 = lean_string_dec_eq(x_3, x_4);
+return x_5;
+}
+else
+{
+uint8_t x_6; 
+x_6 = 0;
+return x_6;
+}
+}
+else
+{
+uint8_t x_7; 
+x_7 = 0;
+return x_7;
+}
+}
+}
+lean_object* l_Lean_Syntax_isQuot___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; lean_object* x_3; 
+x_2 = l_Lean_Syntax_isQuot(x_1);
+lean_dec(x_1);
+x_3 = lean_box(x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Syntax_isAntiquot___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("antiquot");
+return x_1;
+}
+}
+uint8_t l_Lean_Syntax_isAntiquot(lean_object* x_1) {
+_start:
+{
+if (lean_obj_tag(x_1) == 1)
+{
+lean_object* x_2; 
+x_2 = lean_ctor_get(x_1, 0);
+if (lean_obj_tag(x_2) == 1)
+{
+lean_object* x_3; lean_object* x_4; uint8_t x_5; 
+x_3 = lean_ctor_get(x_2, 1);
+x_4 = l_Lean_Syntax_isAntiquot___closed__1;
+x_5 = lean_string_dec_eq(x_3, x_4);
+return x_5;
+}
+else
+{
+uint8_t x_6; 
+x_6 = 0;
+return x_6;
+}
+}
+else
+{
+uint8_t x_7; 
+x_7 = 0;
+return x_7;
+}
+}
+}
+lean_object* l_Lean_Syntax_isAntiquot___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; lean_object* x_3; 
+x_2 = l_Lean_Syntax_isAntiquot(x_1);
+lean_dec(x_1);
+x_3 = lean_box(x_2);
+return x_3;
+}
+}
 lean_object* l_Lean_unreachIsNodeMissing(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@@ -590,7 +692,7 @@ _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_Syntax_getAtomVal_x21___closed__1;
-x_2 = lean_unsigned_to_nat(70u);
+x_2 = lean_unsigned_to_nat(80u);
 x_3 = lean_unsigned_to_nat(16u);
 x_4 = l_Lean_Syntax_getAtomVal_x21___closed__2;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@@ -6407,6 +6509,10 @@ lean_dec_ref(res);
 res = initialize_Lean_Data_Format(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_Syntax_isQuot___closed__1 = _init_l_Lean_Syntax_isQuot___closed__1();
+lean_mark_persistent(l_Lean_Syntax_isQuot___closed__1);
+l_Lean_Syntax_isAntiquot___closed__1 = _init_l_Lean_Syntax_isAntiquot___closed__1();
+lean_mark_persistent(l_Lean_Syntax_isAntiquot___closed__1);
 l_Lean_Syntax_getAtomVal_x21___closed__1 = _init_l_Lean_Syntax_getAtomVal_x21___closed__1();
 lean_mark_persistent(l_Lean_Syntax_getAtomVal_x21___closed__1);
 l_Lean_Syntax_getAtomVal_x21___closed__2 = _init_l_Lean_Syntax_getAtomVal_x21___closed__2();