max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-06 08:21:55 -07:00
parent 10fc908463
commit 514657123b
7 changed files with 413 additions and 334 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
stage0/src/Lean/Elab/Tactic/Basic.lean generated
View file

@ -242,22 +242,21 @@ modifyMCtx fun mctx =>
(mctx, 1);
mctx
def evalSeq : Tactic :=
fun stx => (stx.getArg 0).forArgsM fun seqElem => evalTactic (seqElem.getArg 0)
@[builtinTactic seq1] def evalSeq1 : Tactic := evalSeq
@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := evalSeq
@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic
@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic :=
fun stx => focus $ evalTactic (stx.getArg 1)
@[builtinTactic seq1] def evalSeq1 : Tactic :=
fun stx => (stx.getArg 0).forSepArgsM evalTactic
@[builtinTactic paren] def evalParen : Tactic :=
fun stx => evalSeq1 (stx.getArg 1)
@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic :=
fun stx => (stx.getArg 0).forArgsM fun seqElem => evalTactic (seqElem.getArg 0)
@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forArgsM fun seqElem => evalTactic (seqElem.getArg 0)
@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic :=
fun stx => focus $ evalTactic (stx.getArg 1)
@[builtinTactic tacticSeq] def evalTacticSeq : Tactic :=
fun stx => evalTactic (stx.getArg 0)

2
stage0/src/Lean/Parser/Syntax.lean generated
View file

@ -84,7 +84,7 @@ def optKindPrio : Parser := optional ("[" >> (parserKindPrio <|> parserKind <|>
def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec
def macroArg := try strLit <|> try macroArgSimple
def macroHead := macroArg <|> try ident
def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.tacticSeq1Indented >> ")" <|> termParser)
def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.seq1 >> ")" <|> termParser)
def macroTailCommand : Parser := try (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
def macroTailDefault : Parser := try (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault

2
stage0/src/Lean/Parser/Term.lean generated
View file

@ -260,7 +260,7 @@ stx.isAntiquot || stx.isIdent
end Term
@[builtinTermParser 1] def Tactic.quot : Parser := parser! "`(tactic|" >> toggleInsideQuot tacticParser >> ")"
@[builtinTermParser] def Tactic.quotSeq : Parser := parser! "`(tactic|" >> toggleInsideQuot Tactic.tacticSeq1Indented >> ")"
@[builtinTermParser] def Tactic.quotSeq : Parser := parser! "`(tactic|" >> toggleInsideQuot Tactic.seq1 >> ")"
@[builtinTermParser] def Level.quot : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")"

447
stage0/stdlib/Lean/Elab/Tactic/Basic.c generated
View file

@ -18,6 +18,7 @@ extern lean_object* l___private_Lean_Elab_Binders_12__expandFunBindersAux___main
lean_object* l_Lean_SMap_find_x3f___at_Lean_Elab_Tactic_evalTactic___main___spec__1(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAssumption___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__2;
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalSeq1___spec__1___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* l___regBuiltin_Lean_Elab_Tactic_evalDone___closed__3;
extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
lean_object* l___private_Lean_Elab_Tactic_Basic_2__expandTacticMacroFns___main___closed__9;
@ -46,6 +47,7 @@ extern lean_object* l_Lean_withIncRecDepth___rarg___lambda__2___closed__2;
lean_object* l_Lean_Elab_Tactic_evalIntros___closed__1;
lean_object* l_Lean_Elab_Tactic_withMainMVarContext(lean_object*);
extern lean_object* l_Lean_nullKind;
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeq1Indented___spec__1(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_Basic_4__getIntrosSize___main(lean_object*);
lean_object* l_Lean_Elab_Tactic_monadExcept___closed__2;
lean_object* l_Lean_MetavarContext_instantiateMVars(lean_object*, lean_object*);
@ -193,7 +195,6 @@ lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAssumption(lean_object*);
lean_object* l_Lean_Elab_Tactic_getMainGoal___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_liftMetaTactic___closed__1;
lean_object* l_Lean_Elab_Tactic_try_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTacticSeqBracketed___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_Elab_Tactic_ensureHasNoMVars___boxed(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_Basic_5__sortFVarIds___lambda__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* l_Lean_Elab_Tactic_TacticM_run_x27(lean_object*);
@ -212,7 +213,6 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__19;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalSeq___spec__1(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_Basic_7__regTraceClasses(lean_object*);
lean_object* l_Lean_Meta_getMVarType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprMVarAssigned___at_Lean_Elab_Tactic_pruneSolvedGoals___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -227,6 +227,7 @@ lean_object* l_Lean_Elab_Tactic_evalIntro___closed__3;
extern lean_object* l_Lean_Meta_clear___closed__1;
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Basic_2__expandTacticMacroFns___main___closed__11;
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalSeq1___spec__1(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___regBuiltin_Lean_Elab_Tactic_evalChoice(lean_object*);
lean_object* l_Array_forMAux___main___at_Lean_Elab_Tactic_forEachVar___spec__1___lambda__1(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_Elab_Tactic_focus___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -238,7 +239,6 @@ lean_object* l_Lean_Elab_Tactic_saveBacktrackableState___rarg___boxed(lean_objec
extern lean_object* l___private_Lean_Elab_Term_11__elabUsingElabFns___closed__6;
lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq(lean_object*);
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1(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_Elab_Tactic_TacticM_run(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFailIfSuccess(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFocus___closed__1;
@ -246,7 +246,6 @@ lean_object* l_Std_AssocList_find_x3f___main___at_Lean_Elab_Tactic_evalTactic___
lean_object* l_Lean_Elab_Tactic_SavedState_inhabited;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalTactic___main___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__3;
lean_object* l_Lean_Elab_Tactic_evalSeq___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSkip(lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
@ -345,7 +344,6 @@ lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at___pr
lean_object* l_Lean_Elab_Tactic_try___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_log___at_Lean_Elab_Tactic_evalTactic___main___spec__10___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_Meta_isExprMVarAssigned___at_Lean_Elab_Tactic_pruneSolvedGoals___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1___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*);
size_t l_USize_land(size_t, size_t);
lean_object* l_Lean_Elab_Tactic_evalOrelse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Meta_mkWHNFRef___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -412,7 +410,6 @@ lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at___pr
lean_object* l_Lean_Elab_Tactic_evalIntro___closed__4;
lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_liftMetaTacticAux___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* l_Lean_Elab_Tactic_evalSeq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l_Lean_Elab_logTrace___at_Lean_Elab_Tactic_evalTactic___main___spec__9___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_Elab_Tactic_getFVarId(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -432,6 +429,7 @@ lean_object* l_Lean_Elab_Tactic_setGoals(lean_object*, lean_object*, lean_object
lean_object* l_Lean_Meta_getMVarsImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_saveAllState___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSkip___closed__2;
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1___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* l_Lean_Meta_withMVarContext___at_Lean_Elab_Tactic_withMainMVarContext___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* l_Lean_Elab_Tactic_tagUntaggedGoals(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_Elab_Tactic_focus___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -450,6 +448,7 @@ lean_object* lean_metavar_ctx_find_decl(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalIntro___closed__5;
lean_object* l_Lean_refTrans___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1(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___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRevert(lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Basic_6__findTag_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -460,7 +459,6 @@ lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at___pr
extern lean_object* l___private_Lean_Meta_Check_6__checkApp___closed__5;
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Tactic_Basic_1__evalTacticUsing___main___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* l_Lean_Elab_Tactic_hasOrElse___closed__1;
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalSeq___spec__1___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* l_Lean_Elab_Tactic_monadExcept___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*);
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Tactic_evalIntros___spec__1(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__1;
@ -489,6 +487,7 @@ lean_object* l_Lean_Elab_Tactic_evalDone(lean_object*);
lean_object* l_Lean_setEnv___at_Lean_Elab_Tactic_BacktrackableState_restore___spec__1___boxed(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_Basic_3__introStep(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalIntro(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeq1Indented___spec__1___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*);
extern lean_object* l_Lean_mkHole___closed__2;
lean_object* l_Lean_Elab_Tactic_liftMetaM___rarg___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_Elab_Tactic_try_x3f(lean_object*);
@ -7619,7 +7618,214 @@ lean_dec(x_4);
return x_13;
}
}
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalSeq___spec__1(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalSeq1___spec__1(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
lean_object* x_14; uint8_t x_15;
x_14 = lean_array_get_size(x_2);
x_15 = lean_nat_dec_lt(x_3, x_14);
lean_dec(x_14);
if (x_15 == 0)
{
lean_object* x_16;
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_4);
lean_ctor_set(x_16, 1, x_13);
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18;
lean_dec(x_4);
x_17 = lean_array_fget(x_2, x_3);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_18 = l_Lean_Elab_Tactic_evalTactic___main(x_17, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
lean_dec(x_18);
x_21 = lean_nat_add(x_3, x_1);
lean_dec(x_3);
x_3 = x_21;
x_4 = x_19;
x_13 = x_20;
goto _start;
}
else
{
uint8_t x_23;
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_23 = !lean_is_exclusive(x_18);
if (x_23 == 0)
{
return x_18;
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_18, 0);
x_25 = lean_ctor_get(x_18, 1);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_18);
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
return x_26;
}
}
}
}
}
lean_object* l_Lean_Elab_Tactic_evalSeq1(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_11 = lean_unsigned_to_nat(0u);
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
x_13 = l_Lean_Syntax_getArgs(x_12);
lean_dec(x_12);
x_14 = lean_unsigned_to_nat(2u);
x_15 = lean_box(0);
x_16 = l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalSeq1___spec__1(x_14, x_13, x_11, x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_13);
return x_16;
}
}
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalSeq1___spec__1___boxed(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
lean_object* x_14;
x_14 = l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalSeq1___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
lean_dec(x_2);
lean_dec(x_1);
return x_14;
}
}
lean_object* l_Lean_Elab_Tactic_evalSeq1___boxed(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalSeq1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_1);
return x_11;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("seq1");
return x_1;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1;
x_2 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalSeq1___boxed), 10, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq1(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
x_3 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Tactic_evalParen(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_unsigned_to_nat(1u);
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
x_13 = l_Lean_Elab_Tactic_evalSeq1(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_12);
return x_13;
}
}
lean_object* l_Lean_Elab_Tactic_evalParen___boxed(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalParen(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_1);
return x_11;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1;
x_2 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__19;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalParen___boxed), 10, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalParen(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
x_3 = l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1;
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeq1Indented___spec__1(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
lean_object* x_14; uint8_t x_15;
@ -7710,7 +7916,7 @@ return x_29;
}
}
}
lean_object* l_Lean_Elab_Tactic_evalSeq(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, lean_object* x_9, lean_object* x_10) {
lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
@ -7719,92 +7925,21 @@ x_12 = l_Lean_Syntax_getArg(x_1, x_11);
x_13 = l_Lean_Syntax_getArgs(x_12);
lean_dec(x_12);
x_14 = lean_box(0);
x_15 = l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalSeq___spec__1(x_1, x_13, x_11, x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_15 = l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeq1Indented___spec__1(x_1, x_13, x_11, x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_13);
return x_15;
}
}
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalSeq___spec__1___boxed(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeq1Indented___spec__1___boxed(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
lean_object* x_14;
x_14 = l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalSeq___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
x_14 = l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeq1Indented___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
lean_dec(x_2);
lean_dec(x_1);
return x_14;
}
}
lean_object* l_Lean_Elab_Tactic_evalSeq___boxed(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalSeq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_1);
return x_11;
}
}
lean_object* l_Lean_Elab_Tactic_evalSeq1(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalSeq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_11;
}
}
lean_object* l_Lean_Elab_Tactic_evalSeq1___boxed(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalSeq1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_1);
return x_11;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("seq1");
return x_1;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1;
x_2 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalSeq1___boxed), 10, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq1(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
x_3 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalSeq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_11;
}
}
lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented___boxed(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, lean_object* x_9, lean_object* x_10) {
_start:
{
@ -7833,7 +7968,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
lean_object* x_14; uint8_t x_15;
@ -7859,9 +7994,15 @@ return x_16;
}
else
{
lean_object* x_17; lean_object* x_18;
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_dec(x_4);
x_17 = lean_array_fget(x_2, x_3);
x_18 = lean_unsigned_to_nat(1u);
x_19 = lean_nat_add(x_3, x_18);
lean_dec(x_3);
x_20 = lean_unsigned_to_nat(0u);
x_21 = l_Lean_Syntax_getArg(x_17, x_20);
lean_dec(x_17);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
@ -7870,25 +8011,24 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_18 = l_Lean_Elab_Tactic_evalTactic___main(x_17, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_18) == 0)
x_22 = l_Lean_Elab_Tactic_evalTactic___main(x_21, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
lean_dec(x_18);
x_21 = lean_nat_add(x_3, x_1);
lean_dec(x_3);
x_3 = x_21;
x_4 = x_19;
x_13 = x_20;
lean_object* x_23; lean_object* x_24;
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_3 = x_19;
x_4 = x_23;
x_13 = x_24;
goto _start;
}
else
{
uint8_t x_23;
uint8_t x_26;
lean_dec(x_19);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
@ -7897,24 +8037,23 @@ lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_23 = !lean_is_exclusive(x_18);
if (x_23 == 0)
x_26 = !lean_is_exclusive(x_22);
if (x_26 == 0)
{
return x_18;
return x_22;
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_18, 0);
x_25 = lean_ctor_get(x_18, 1);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_18);
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
return x_26;
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_22, 0);
x_28 = lean_ctor_get(x_22, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_22);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
}
}
}
@ -7932,8 +8071,8 @@ x_15 = l_Lean_Syntax_getArgs(x_14);
lean_dec(x_14);
x_16 = lean_unsigned_to_nat(0u);
x_17 = lean_box(0);
x_18 = lean_alloc_closure((void*)(l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1___boxed), 13, 4);
lean_closure_set(x_18, 0, x_11);
x_18 = lean_alloc_closure((void*)(l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1___boxed), 13, 4);
lean_closure_set(x_18, 0, x_1);
lean_closure_set(x_18, 1, x_15);
lean_closure_set(x_18, 2, x_16);
lean_closure_set(x_18, 3, x_17);
@ -7982,25 +8121,16 @@ return x_33;
}
}
}
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1___boxed(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1___boxed(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
lean_object* x_14;
x_14 = l_Array_foldlStepMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
x_14 = l_Array_iterateMAux___main___at_Lean_Elab_Tactic_evalTacticSeqBracketed___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
lean_dec(x_2);
lean_dec(x_1);
return x_14;
}
}
lean_object* l_Lean_Elab_Tactic_evalTacticSeqBracketed___boxed(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalTacticSeqBracketed(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_1);
return x_11;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__1() {
_start:
{
@ -8023,7 +8153,7 @@ lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___clos
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTacticSeqBracketed___boxed), 10, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTacticSeqBracketed), 10, 0);
return x_1;
}
}
@ -8096,55 +8226,6 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Tactic_evalParen(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_unsigned_to_nat(1u);
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
x_13 = l_Lean_Elab_Tactic_evalSeq(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_12);
return x_13;
}
}
lean_object* l_Lean_Elab_Tactic_evalParen___boxed(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, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalParen(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_1);
return x_11;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1;
x_2 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__19;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalParen___boxed), 10, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalParen(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
x_3 = l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1;
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Tactic_evalTacticSeq(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, lean_object* x_9, lean_object* x_10) {
_start:
{
@ -15330,6 +15411,13 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3);
res = l___regBuiltin_Lean_Elab_Tactic_evalSeq1(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1);
l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2);
res = l___regBuiltin_Lean_Elab_Tactic_evalParen(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1);
res = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented(lean_io_mk_world());
@ -15353,13 +15441,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalFocus___closed__3);
res = l___regBuiltin_Lean_Elab_Tactic_evalFocus(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1);
l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2);
res = l___regBuiltin_Lean_Elab_Tactic_evalParen(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__1);
l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__2();

12
stage0/stdlib/Lean/Parser/Syntax.c generated
View file

@ -21,6 +21,7 @@ lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_optKindPrio_formatter___closed__7;
lean_object* l_Lean_Parser_Syntax_cat___closed__6;
lean_object* l_Lean_Parser_Syntax_notFollowedBy_formatter___closed__2;
extern lean_object* l_Lean_Parser_Tactic_seq1___closed__3;
lean_object* l_Lean_Parser_Syntax_orelse___closed__5;
lean_object* l_Lean_Parser_Command_syntax_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Term_stx_quot_parenthesizer(lean_object*);
@ -264,6 +265,7 @@ extern lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Term_stx_quot(lean_object*);
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__7;
lean_object* l_Lean_Parser_Syntax_atom_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_quotSeq_formatter___closed__4;
lean_object* l_Lean_Parser_Command_macroArgSimple___closed__1;
lean_object* l_Lean_Parser_registerBuiltinDynamicParserAttribute(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_try___closed__7;
@ -572,7 +574,6 @@ lean_object* l_Lean_Parser_Command_macroTailTactic_parenthesizer(lean_object*, l
lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__4;
extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__1;
lean_object* l_Lean_Parser_Command_postfix;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___closed__10;
lean_object* l_Lean_Parser_Command_infix___closed__2;
lean_object* l_Lean_Parser_Command_parserKindPrio___elambda__1___closed__4;
lean_object* l___regBuiltin_Lean_Parser_Syntax_notFollowedBy_parenthesizer___closed__1;
@ -832,7 +833,6 @@ lean_object* l_Lean_Parser_registerBuiltinParserAttribute(lean_object*, lean_obj
lean_object* l_Lean_Parser_Command_optKindPrio_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Command_elab___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_macroTailCommand_formatter___closed__5;
extern lean_object* l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Syntax_char___elambda__1___closed__1;
lean_object* l_Lean_Parser_Syntax_sepBy1___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_macroTailCommand_parenthesizer___closed__2;
@ -853,7 +853,6 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Syntax_paren___elambd
lean_object* l_Lean_Parser_Command_notationItem___closed__2;
lean_object* l_Lean_Parser_Command_elab__rules___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_reserve___closed__1;
extern lean_object* l_Lean_Parser_Tactic_quotSeq_formatter___closed__3;
lean_object* l_Lean_Parser_Command_optKindPrio_formatter___closed__4;
lean_object* l_Lean_Parser_Command_mixfixKind_formatter___closed__3;
lean_object* l_Lean_Parser_Syntax_atom_formatter___closed__2;
@ -1082,6 +1081,7 @@ lean_object* l_Lean_Parser_categoryParser(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_prefix___closed__5;
lean_object* l_Lean_Parser_Syntax_many1___closed__3;
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_syntax_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Command_parserPrio_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -23438,7 +23438,7 @@ lean_inc(x_23);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__10;
x_24 = l_Lean_Parser_Tactic_seq1___closed__3;
lean_inc(x_1);
x_25 = l_Lean_Parser_toggleInsideQuotFn(x_24, x_1, x_22);
x_26 = lean_ctor_get(x_25, 3);
@ -25617,7 +25617,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_quot_formatter___closed__2;
x_2 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__3;
x_2 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -26175,7 +26175,7 @@ lean_object* _init_l_Lean_Parser_Command_macroTailTactic_parenthesizer___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__4;
x_1 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__5;
x_2 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__1;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);

123
stage0/stdlib/Lean/Parser/Tactic.c generated
View file

@ -113,10 +113,8 @@ lean_object* l_Lean_Parser_Tactic_have___closed__4;
lean_object* l_Lean_Parser_Tactic_generalize___closed__2;
lean_object* l_Lean_Parser_Tactic_matchAlt___closed__6;
lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_paren_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Tactic_locationWildcard_parenthesizer___closed__2;
extern lean_object* l_Lean_Parser_notFollowedByFn___closed__1;
lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_traceState_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__5;
lean_object* l_Lean_Parser_Tactic_intro___closed__9;
@ -146,7 +144,6 @@ lean_object* l_Lean_Parser_Tactic_changeWith___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_rwRuleSeq_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Tactic_match___closed__10;
lean_object* l_Lean_Parser_Tactic_clear_parenthesizer___closed__2;
extern lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed_parenthesizer___closed__2;
lean_object* l_Lean_PrettyPrinter_Formatter_many_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_injection___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Tactic_rewriteSeq_parenthesizer___closed__1;
@ -280,7 +277,6 @@ lean_object* l_Lean_Parser_Tactic_inductionAlt;
lean_object* l_Lean_Parser_Tactic_assumption_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_generalizingVars_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_skip_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_seq1_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_rwRuleSeq___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_matchAlts___closed__4;
lean_object* l_Lean_Parser_Tactic_injection_formatter___closed__3;
@ -505,7 +501,6 @@ lean_object* l_Lean_Parser_Tactic_inductionAlt_parenthesizer(lean_object*, lean_
lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_skip_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_refine_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_intros_parenthesizer___closed__2;
lean_object* l_Lean_PrettyPrinter_Formatter_trailingNode_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean___kind_term____x40_Lean_Util_Trace___hyg_3____closed__15;
@ -553,7 +548,6 @@ lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__8;
lean_object* l_Lean_Parser_Tactic_location_formatter___closed__6;
lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__10;
lean_object* l_Lean_Parser_Tactic_inductionAlt_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_seq1_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_admit_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_location___closed__6;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -736,6 +730,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Tactic_let_x21(lean_object*);
lean_object* l_Lean_Parser_Tactic_changeWith_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_admit___elambda__1___closed__3;
lean_object* l_Lean_Parser_Tactic_seq1___elambda__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_assumption___closed__6;
extern lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__1;
lean_object* l_Lean_Parser_Tactic_induction_formatter___closed__7;
@ -744,7 +739,6 @@ lean_object* l_Lean_Parser_Tactic_induction___closed__7;
lean_object* l_Lean_Parser_Tactic_revert___closed__5;
lean_object* l_Lean_PrettyPrinter_Formatter_node_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__9;
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__7;
lean_object* l_Lean_Parser_Tactic_rwRuleSeq_formatter___closed__4;
lean_object* l_Lean_Parser_Tactic_induction_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1061,7 +1055,6 @@ lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Tactic_let_formatter(lean_object*);
lean_object* l_Lean_Parser_Tactic_case_parenthesizer___closed__4;
lean_object* l___regBuiltin_Lean_Parser_Tactic_assumption_formatter___closed__1;
extern lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_location_parenthesizer___closed__8;
lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__8;
lean_object* l___regBuiltin_Lean_Parser_Tactic_show_formatter(lean_object*);
@ -1071,7 +1064,6 @@ extern lean_object* l_Lean_Parser_antiquotNestedExpr_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_failIfSuccess___elambda__1___closed__6;
lean_object* l_Lean_Parser_Tactic_suffices___closed__5;
lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_paren_formatter___closed__5;
lean_object* l_Lean_Parser_Tactic_intros___closed__4;
extern lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_tupleTail___elambda__1___spec__2___closed__4;
lean_object* l_Lean_Parser_Tactic_rewrite___elambda__1(lean_object*, lean_object*);
@ -1449,6 +1441,7 @@ lean_object* l_Lean_Parser_Tactic_intros_formatter___closed__7;
lean_object* l_Lean_Parser_Tactic_let_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_injection;
lean_object* l_Lean_Parser_Tactic_induction_formatter___closed__9;
extern lean_object* l_Lean_Parser_Tactic_quotSeq_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_exact___closed__2;
lean_object* l_Lean_Parser_Tactic_suffices___elambda__1___closed__3;
lean_object* l_Lean_Parser_Tactic_rewrite_parenthesizer___closed__7;
@ -27980,28 +27973,6 @@ 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() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__5;
x_2 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_sepBy1_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_seq1_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_7 = l_Lean_Parser_Tactic_seq1_formatter___closed__1;
x_8 = l_Lean_PrettyPrinter_Formatter_node_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
}
lean_object* _init_l_Lean_Parser_Tactic_paren_formatter___closed__1() {
_start:
{
@ -28020,17 +27991,21 @@ return x_5;
lean_object* _init_l_Lean_Parser_Tactic_paren_formatter___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_seq1_formatter), 5, 0);
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__2;
x_2 = l_Lean_Parser_antiquotNestedExpr_formatter___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 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_paren_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_paren_formatter___closed__2;
x_2 = l_Lean_Parser_antiquotNestedExpr_formatter___closed__4;
x_1 = l_Lean_Parser_antiquotNestedExpr_formatter___closed__1;
x_2 = l_Lean_Parser_Tactic_paren_formatter___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -28040,22 +28015,10 @@ return x_3;
lean_object* _init_l_Lean_Parser_Tactic_paren_formatter___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_formatter___closed__1;
x_2 = l_Lean_Parser_Tactic_paren_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 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_paren_formatter___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_paren_formatter___closed__4;
x_3 = l_Lean_Parser_Tactic_paren_formatter___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -28068,7 +28031,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_paren_formatter___closed__1;
x_7 = l_Lean_Parser_Tactic_paren_formatter___closed__5;
x_7 = l_Lean_Parser_Tactic_paren_formatter___closed__4;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -28092,28 +28055,6 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_tacticSeqBracketed_parenthesizer___closed__2;
x_2 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_sepBy1_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_7 = l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
}
lean_object* _init_l_Lean_Parser_Tactic_paren_parenthesizer___closed__1() {
_start:
{
@ -28130,17 +28071,21 @@ return x_4;
lean_object* _init_l_Lean_Parser_Tactic_paren_parenthesizer___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_seq1_parenthesizer), 5, 0);
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__2;
x_2 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 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_paren_parenthesizer___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_paren_parenthesizer___closed__2;
x_2 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Tactic_paren_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -28150,22 +28095,10 @@ return x_3;
lean_object* _init_l_Lean_Parser_Tactic_paren_parenthesizer___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Tactic_paren_parenthesizer___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 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_paren_parenthesizer___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_paren_parenthesizer___closed__4;
x_3 = l_Lean_Parser_Tactic_paren_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -28178,7 +28111,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_paren_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Tactic_paren_parenthesizer___closed__5;
x_7 = l_Lean_Parser_Tactic_paren_parenthesizer___closed__4;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -33553,8 +33486,6 @@ lean_mark_persistent(l_Lean_Parser_Tactic_paren);
res = l___regBuiltinParser_Lean_Parser_Tactic_paren(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Tactic_seq1_formatter___closed__1 = _init_l_Lean_Parser_Tactic_seq1_formatter___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1_formatter___closed__1);
l_Lean_Parser_Tactic_paren_formatter___closed__1 = _init_l_Lean_Parser_Tactic_paren_formatter___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_paren_formatter___closed__1);
l_Lean_Parser_Tactic_paren_formatter___closed__2 = _init_l_Lean_Parser_Tactic_paren_formatter___closed__2();
@ -33563,15 +33494,11 @@ l_Lean_Parser_Tactic_paren_formatter___closed__3 = _init_l_Lean_Parser_Tactic_pa
lean_mark_persistent(l_Lean_Parser_Tactic_paren_formatter___closed__3);
l_Lean_Parser_Tactic_paren_formatter___closed__4 = _init_l_Lean_Parser_Tactic_paren_formatter___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_paren_formatter___closed__4);
l_Lean_Parser_Tactic_paren_formatter___closed__5 = _init_l_Lean_Parser_Tactic_paren_formatter___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_paren_formatter___closed__5);
l___regBuiltin_Lean_Parser_Tactic_paren_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_paren_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_paren_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_paren_formatter(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1);
l_Lean_Parser_Tactic_paren_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_paren_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_paren_parenthesizer___closed__1);
l_Lean_Parser_Tactic_paren_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_paren_parenthesizer___closed__2();
@ -33580,8 +33507,6 @@ l_Lean_Parser_Tactic_paren_parenthesizer___closed__3 = _init_l_Lean_Parser_Tacti
lean_mark_persistent(l_Lean_Parser_Tactic_paren_parenthesizer___closed__3);
l_Lean_Parser_Tactic_paren_parenthesizer___closed__4 = _init_l_Lean_Parser_Tactic_paren_parenthesizer___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_paren_parenthesizer___closed__4);
l_Lean_Parser_Tactic_paren_parenthesizer___closed__5 = _init_l_Lean_Parser_Tactic_paren_parenthesizer___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_paren_parenthesizer___closed__5);
l___regBuiltin_Lean_Parser_Tactic_paren_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_paren_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_paren_parenthesizer___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_paren_parenthesizer(lean_io_mk_world());

138
stage0/stdlib/Lean/Parser/Term.c generated
View file

@ -248,6 +248,7 @@ lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__2;
lean_object* l_Lean_Parser_Tactic_quot___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_show___elambda__1___closed__5;
extern lean_object* l_Array_iterateMAux___main___at_Lean_ppGoal___spec__6___closed__3;
lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_mapRev_formatter___closed__1;
lean_object* l_Lean_Parser_Term_fun_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__7;
@ -696,6 +697,7 @@ lean_object* l_Lean_Parser_Term_matchAlts___closed__6;
lean_object* l_Lean_Parser_Term_fun_parenthesizer___closed__8;
lean_object* l_Lean_Parser_Term_namedArgument___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_paren_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_seq1_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_nativeDecide_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_namedArgument___closed__3;
lean_object* l_Lean_Parser_Term_dollarProj_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1226,6 +1228,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_quot_formatter___closed__1;
lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__8;
lean_object* l_Lean_Parser_Term_ensureTypeOf___elambda__1___closed__9;
extern lean_object* l_Lean_Parser_mkAntiquot___closed__5;
lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_funBinder_quot___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_typeOf___elambda__1___closed__8;
lean_object* l_Lean_PrettyPrinter_Formatter_trailingNode_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1335,6 +1338,7 @@ lean_object* l_Lean_Parser_Term_structInstLVal_formatter___closed__4;
lean_object* l_Lean_Parser_Term_lt___closed__3;
lean_object* l_Lean_Parser_Term_div___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_sorry___elambda__1___closed__2;
lean_object* l_Lean_Parser_Tactic_seq1_formatter___closed__1;
lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2(uint8_t, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_not_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_not___elambda__1___closed__6;
@ -2087,6 +2091,7 @@ lean_object* l_Lean_Parser_Term_seq;
lean_object* l_Lean_Parser_Term_show___closed__8;
lean_object* l_Lean_Parser_Term_matchAlts_parenthesizer___closed__9;
lean_object* l_Lean_Parser_Term_depArrow___closed__1;
lean_object* l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Term_proj___closed__5;
lean_object* l_Lean_Parser_Term_letIdDecl_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_nativeDecide___elambda__1___closed__3;
@ -3728,6 +3733,7 @@ lean_object* l_Lean_Parser_Term_beq___closed__1;
lean_object* l_Lean_Parser_Term_fun___closed__2;
lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_if_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_quotSeq_formatter___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Term_hole(lean_object*);
lean_object* l_Lean_Parser_Term_iff___closed__2;
lean_object* l_Lean_Parser_Term_orelse___closed__4;
@ -83419,7 +83425,7 @@ lean_inc(x_12);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__10;
x_13 = l_Lean_Parser_Tactic_seq1___closed__3;
lean_inc(x_1);
x_14 = l_Lean_Parser_toggleInsideQuotFn(x_13, x_1, x_11);
x_15 = lean_ctor_get(x_14, 3);
@ -83635,7 +83641,7 @@ lean_inc(x_72);
if (lean_obj_tag(x_72) == 0)
{
lean_object* x_73; lean_object* x_74; lean_object* x_75;
x_73 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__10;
x_73 = l_Lean_Parser_Tactic_seq1___closed__3;
lean_inc(x_1);
x_74 = l_Lean_Parser_toggleInsideQuotFn(x_73, x_1, x_71);
x_75 = lean_ctor_get(x_74, 3);
@ -83831,6 +83837,28 @@ 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() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__5;
x_2 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_sepBy1_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_seq1_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_7 = l_Lean_Parser_Tactic_seq1_formatter___closed__1;
x_8 = l_Lean_PrettyPrinter_Formatter_node_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
}
lean_object* _init_l_Lean_Parser_Tactic_quotSeq_formatter___closed__1() {
_start:
{
@ -83849,31 +83877,27 @@ return x_5;
lean_object* _init_l_Lean_Parser_Tactic_quotSeq_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_tacticSeq_formatter___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_toggleInsideQuot_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_seq1_formatter), 5, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_quotSeq_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__2;
x_2 = l_Lean_Parser_antiquotNestedExpr_formatter___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_toggleInsideQuot_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Tactic_quotSeq_formatter___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_quot_formatter___closed__2;
x_2 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__3;
x_1 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__3;
x_2 = l_Lean_Parser_antiquotNestedExpr_formatter___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -83883,10 +83907,22 @@ return x_3;
lean_object* _init_l_Lean_Parser_Tactic_quotSeq_formatter___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_quot_formatter___closed__2;
x_2 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 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_quotSeq_formatter___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_quotSeq___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__4;
x_3 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__5;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -83899,7 +83935,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__1;
x_7 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__5;
x_7 = l_Lean_Parser_Tactic_quotSeq_formatter___closed__6;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -83923,6 +83959,28 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_tacticSeqBracketed_parenthesizer___closed__2;
x_2 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_sepBy1_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_7 = l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
}
lean_object* _init_l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__1() {
_start:
{
@ -83939,31 +83997,27 @@ return x_4;
lean_object* _init_l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_tacticSeq_parenthesizer___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_toggleInsideQuot_parenthesizer), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_seq1_parenthesizer), 5, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__2;
x_2 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_toggleInsideQuot_parenthesizer), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__3;
x_1 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__3;
x_2 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -83973,10 +84027,22 @@ return x_3;
lean_object* _init_l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 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_quotSeq_parenthesizer___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_quotSeq___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__4;
x_3 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__5;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -83989,7 +84055,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__5;
x_7 = l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__6;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -91765,6 +91831,8 @@ lean_mark_persistent(l_Lean_Parser_Tactic_quotSeq);
res = l___regBuiltinParser_Lean_Parser_Tactic_quotSeq(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Tactic_seq1_formatter___closed__1 = _init_l_Lean_Parser_Tactic_seq1_formatter___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1_formatter___closed__1);
l_Lean_Parser_Tactic_quotSeq_formatter___closed__1 = _init_l_Lean_Parser_Tactic_quotSeq_formatter___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_quotSeq_formatter___closed__1);
l_Lean_Parser_Tactic_quotSeq_formatter___closed__2 = _init_l_Lean_Parser_Tactic_quotSeq_formatter___closed__2();
@ -91775,11 +91843,15 @@ l_Lean_Parser_Tactic_quotSeq_formatter___closed__4 = _init_l_Lean_Parser_Tactic_
lean_mark_persistent(l_Lean_Parser_Tactic_quotSeq_formatter___closed__4);
l_Lean_Parser_Tactic_quotSeq_formatter___closed__5 = _init_l_Lean_Parser_Tactic_quotSeq_formatter___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_quotSeq_formatter___closed__5);
l_Lean_Parser_Tactic_quotSeq_formatter___closed__6 = _init_l_Lean_Parser_Tactic_quotSeq_formatter___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_quotSeq_formatter___closed__6);
l___regBuiltin_Lean_Parser_Tactic_quotSeq_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_quotSeq_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_quotSeq_formatter___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_quotSeq_formatter(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1);
l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__1);
l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__2();
@ -91790,6 +91862,8 @@ l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__4 = _init_l_Lean_Parser_Tac
lean_mark_persistent(l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__4);
l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__5 = _init_l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__5);
l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__6 = _init_l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__6);
l___regBuiltin_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_quotSeq_parenthesizer___closed__1);
res = l___regBuiltin_Lean_Parser_Tactic_quotSeq_parenthesizer(lean_io_mk_world());