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-09-28 15:47:58 -07:00
parent 7f9013e496
commit c7b5422929
7 changed files with 165 additions and 134 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -243,17 +243,19 @@ modifyMCtx fun mctx =>
(mctx, 1);
mctx
@[builtinTactic seq] def evalSeq : Tactic :=
def evalSeq : Tactic :=
fun stx => (stx.getArg 0).forSepArgsM evalTactic
@[builtinTactic seq1] def evalSeq1 : Tactic := evalSeq
@[builtinTactic paren] def evalParen : Tactic :=
fun stx => evalSeq1 (stx.getArg 1)
@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := evalSeq
@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic
@[builtinTactic paren] def evalParen : Tactic :=
fun stx => evalSeq1 (stx.getArg 1)
@[builtinTactic tacticSeq] def evalTacticSeq : Tactic :=
fun stx => evalTactic (stx.getArg 0)

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

@ -256,7 +256,7 @@ stx.isAntiquot || stx.isIdent
end Term
def Tactic.seq1Unbox := nodeSepBy1Unbox `Lean.Parser.Tactic.seq tacticParser "; " true
def Tactic.seq1Unbox := nodeSepBy1Unbox `Lean.Parser.Tactic.seq1 tacticParser "; " true
@[builtinTermParser] def Tactic.quot : Parser := parser! "`(tactic|" >> toggleInsideQuot Tactic.seq1Unbox >> ")"
@[builtinTermParser] def Level.quot : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")"

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

@ -38,6 +38,7 @@ lean_object* l_Lean_Elab_Tactic_withMainMVarContext___rarg(lean_object*, lean_ob
lean_object* l_Lean_Elab_Tactic_mkTacticAttribute___closed__3;
lean_object* lean_nat_div(lean_object*, lean_object*);
extern lean_object* l_Lean_KeyedDeclsAttribute_KeyedDeclsAttribute_inhabited___closed__1;
lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_withIncRecDepth___rarg___lambda__2___closed__2;
lean_object* l_Lean_Elab_Tactic_evalIntros___closed__1;
@ -92,6 +93,7 @@ lean_object* l_Lean_Elab_Tactic_liftMetaM___rarg(lean_object*, lean_object*, lea
lean_object* l_Lean_Elab_Tactic_evalCase___closed__1;
lean_object* l_Lean_Elab_Tactic_done(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkMVar(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Array_empty___closed__1;
extern lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1;
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
@ -122,6 +124,7 @@ lean_object* l_ReaderT_bind___at_Lean_Meta_Lean_MonadLCtx___spec__2___rarg(lean_
lean_object* l_Lean_Elab_Tactic_ensureHasType___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_evalIntro(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_evalCase___closed__5;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3;
lean_object* l_Lean_Elab_Tactic_evalCase___closed__3;
lean_object* l___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___closed__1;
lean_object* l_Lean_Meta_getMVars___at_Lean_Elab_Tactic_ensureHasNoMVars___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -139,6 +142,7 @@ lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Elab_Tactic_evalTactic__
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalDone___rarg(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_evalTacticSeq1Indented(lean_object*);
lean_object* l_Lean_MetavarContext_renameMVar(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_reportUnsolvedGoals___closed__3;
lean_object* l_Lean_Elab_Tactic_mkTacticAttribute___closed__4;
@ -194,7 +198,6 @@ lean_object* l_Lean_Elab_Tactic_try_x3f___rarg(lean_object*, lean_object*, lean_
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___regBuiltin_Lean_Elab_Tactic_evalSeq(lean_object*);
lean_object* l_Lean_Elab_Tactic_TacticM_run_x27(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDone___closed__1;
lean_object* l_Lean_Meta_intro1Core(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -235,13 +238,13 @@ 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_Lean_Elab_Tactic_TacticM_run(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFailIfSuccess(lean_object*);
lean_object* l_Std_AssocList_find_x3f___main___at_Lean_Elab_Tactic_evalTactic___main___spec__6(lean_object*, lean_object*);
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_evalTacticSeq1Indented___closed__2;
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*);
@ -271,6 +274,7 @@ size_t l_Lean_Name_hash(lean_object*);
lean_object* l_Lean_Elab_Tactic_getMainGoal___closed__1;
lean_object* l_List_erase___main___at_Lean_Elab_Tactic_evalCase___spec__1___boxed(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalChoice___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAssumption___closed__1;
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDone___closed__2;
@ -7732,25 +7736,6 @@ lean_dec(x_1);
return x_11;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalSeq___boxed), 10, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq(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___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux___main___closed__7;
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
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:
{
@ -7805,51 +7790,56 @@ 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) {
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_evalParen(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
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:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalTacticSeq1Indented(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() {
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("tacticSeq1Indented");
return x_1;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___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_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__19;
x_2 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2() {
lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalParen___boxed), 10, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTacticSeq1Indented___boxed), 10, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalParen(lean_object* x_1) {
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented(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_3 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
@ -7962,6 +7952,55 @@ 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:
{
@ -15115,11 +15154,6 @@ if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Tactic_focus___rarg___closed__1 = _init_l_Lean_Elab_Tactic_focus___rarg___closed__1();
lean_mark_persistent(l_Lean_Elab_Tactic_focus___rarg___closed__1);
l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1);
res = l___regBuiltin_Lean_Elab_Tactic_evalSeq(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1);
l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2();
@ -15129,11 +15163,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());
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);
l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__2);
l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3);
res = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__1();
@ -15145,6 +15181,13 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___cl
res = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed(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();

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

@ -151,6 +151,7 @@ lean_object* l___regBuiltin_Lean_Parser_Syntax_num_formatter(lean_object*);
lean_object* l_Lean_Parser_Syntax_try_formatter___closed__4;
lean_object* l_Lean_Parser_Command_macroHead;
lean_object* l_Lean_Parser_Command_mixfix_parenthesizer___closed__10;
extern lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__2;
lean_object* l_Lean_Parser_Syntax_paren___closed__4;
lean_object* l_Lean_Parser_Command_elab_parenthesizer___closed__10;
lean_object* l_Lean_Parser_Syntax_many1___elambda__1___closed__2;
@ -430,7 +431,6 @@ lean_object* l_Lean_Parser_Syntax_ident___closed__5;
lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_notation___closed__6;
lean_object* l_Lean_Parser_Command_infixl_formatter___closed__2;
extern lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__3;
lean_object* l_Lean_Parser_Command_mixfix___closed__9;
lean_object* l_Lean_Parser_Syntax_try_parenthesizer___closed__4;
lean_object* l_Lean_Parser_maxSymbol_formatter___closed__3;
@ -23476,7 +23476,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_seq1Unbox___closed__3;
x_24 = l_Lean_Parser_Tactic_seq1Unbox___closed__2;
lean_inc(x_1);
x_25 = l_Lean_Parser_toggleInsideQuotFn(x_24, x_1, x_22);
x_26 = lean_ctor_get(x_25, 3);

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

@ -733,6 +733,7 @@ lean_object* l_Lean_Parser_Tactic_revert___closed__5;
extern lean_object* l_Lean_Parser_Term_have_parenthesizer___closed__2;
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*);
@ -1696,7 +1697,6 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer(lean_object*,
lean_object* l_Lean_Parser_Tactic_admit_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_introMatch_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__3;
extern lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
lean_object* l_Lean_Parser_Tactic_rewrite_formatter___closed__8;
lean_object* l_Lean_Parser_andthenFn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Tactic_paren_formatter(lean_object*);
@ -26568,7 +26568,7 @@ lean_object* l_Lean_Parser_Tactic_seq1_formatter(lean_object* x_1, lean_object*
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
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;
@ -26680,7 +26680,7 @@ lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer(lean_object* x_1, lean_obje
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
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;

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

@ -624,7 +624,6 @@ lean_object* l_Lean_Parser_Term_bracketedBinder_formatter___boxed(lean_object*,
lean_object* l_Lean_Parser_Level_quot_formatter___closed__2;
lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_letrec_formatter___closed__5;
lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__1;
lean_object* l_Lean_Parser_nonReservedSymbolFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_beq___elambda__1___closed__4;
@ -1755,6 +1754,7 @@ lean_object* l_Lean_Parser_Term_subtype;
lean_object* l_Lean_PrettyPrinter_Formatter_node_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Term_depArrow_formatter___closed__1;
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_Term_nativeDecide___closed__5;
lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_match_formatter___closed__1;
@ -2612,7 +2612,6 @@ lean_object* l_Lean_Parser_Term_byTactic___closed__5;
lean_object* l_Lean_Parser_Term_proj___closed__7;
lean_object* l_Lean_Parser_Term_app_formatter___closed__1;
lean_object* l_Lean_Parser_Term_if___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__4;
lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__12;
lean_object* l_Lean_Parser_Term_decide___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_str_parenthesizer___closed__1;
@ -3286,7 +3285,6 @@ lean_object* l_Lean_Parser_Term_app___closed__1;
lean_object* l_Lean_Parser_Term_emptyC___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Term_have_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_unreachable_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_panic_formatter___closed__1;
lean_object* l_Lean_Parser_Term_mod_formatter___closed__1;
lean_object* l_Lean_Parser_Term_attrInstance_formatter___closed__1;
@ -4111,7 +4109,6 @@ lean_object* l_Lean_Parser_Term_explicitBinder_formatter___closed__5;
lean_object* l_Lean_Parser_Term_namedArgument_formatter___closed__3;
lean_object* l_Lean_Parser_Term_letrec_formatter___closed__8;
lean_object* l_Lean_Parser_Term_let_x21___closed__4;
lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_match_formatter___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Term_andthen_formatter(lean_object*);
uint8_t l_Lean_Syntax_isIdent(lean_object*);
@ -5945,24 +5942,6 @@ x_7 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic
return x_7;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("seq1");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2;
x_2 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_seq1___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -5973,7 +5952,7 @@ x_4 = lean_array_get_size(x_3);
lean_dec(x_3);
x_5 = 1;
x_6 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(x_5, x_1, x_2);
x_7 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
x_7 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_8 = l_Lean_Parser_ParserState_mkNode(x_6, x_7, x_4);
return x_8;
}
@ -5994,7 +5973,7 @@ lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_2 = l_Lean_Parser_Tactic_seq1___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -76343,16 +76322,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_seq1Unbox___elambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2;
x_2 = l_Lean_Parser_Term_seq___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_seq1Unbox___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -76363,7 +76332,7 @@ x_4 = lean_array_get_size(x_3);
lean_dec(x_3);
x_5 = 1;
x_6 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(x_5, x_1, x_2);
x_7 = l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1;
x_7 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_8 = l_Lean_Parser_ParserState_mkNode(x_6, x_7, x_4);
x_9 = lean_ctor_get(x_8, 3);
lean_inc(x_9);
@ -76408,23 +76377,13 @@ return x_8;
lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1;
x_2 = l_Lean_Parser_Tactic_seq1___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__1;
x_1 = l_Lean_Parser_Tactic_seq1___closed__2;
x_2 = l_Lean_Parser_withResultOfInfo(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__3() {
lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__2() {
_start:
{
lean_object* x_1;
@ -76432,12 +76391,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_seq1Unbox___elambda__1), 2
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__4() {
lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__2;
x_2 = l_Lean_Parser_Tactic_seq1Unbox___closed__3;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__1;
x_2 = l_Lean_Parser_Tactic_seq1Unbox___closed__2;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -76448,7 +76407,7 @@ lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__4;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__3;
return x_1;
}
}
@ -76621,7 +76580,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_seq1Unbox___closed__3;
x_13 = l_Lean_Parser_Tactic_seq1Unbox___closed__2;
lean_inc(x_1);
x_14 = l_Lean_Parser_toggleInsideQuotFn(x_13, x_1, x_11);
x_15 = lean_ctor_get(x_14, 3);
@ -76837,7 +76796,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_seq1Unbox___closed__3;
x_73 = l_Lean_Parser_Tactic_seq1Unbox___closed__2;
lean_inc(x_1);
x_74 = l_Lean_Parser_toggleInsideQuotFn(x_73, x_1, x_71);
x_75 = lean_ctor_get(x_74, 3);
@ -77056,7 +77015,7 @@ lean_object* l_Lean_Parser_Tactic_seq1Unbox_formatter(lean_object* x_1, lean_obj
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1;
x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_7 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__4;
x_8 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__3;
x_9 = l_Lean_PrettyPrinter_Formatter_nodeSepBy1Unbox_formatter(x_6, x_7, x_8, x_1, x_2, x_3, x_4, x_5);
@ -77177,7 +77136,7 @@ lean_object* l_Lean_Parser_Tactic_seq1Unbox_parenthesizer(lean_object* x_1, lean
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1;
x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_7 = l_Lean_Parser_Tactic_tacticSeqBracketed_parenthesizer___closed__2;
x_8 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_9 = l_Lean_PrettyPrinter_Parenthesizer_nodeSepBy1Unbox_parenthesizer(x_6, x_7, x_8, x_1, x_2, x_3, x_4, x_5);
@ -78215,10 +78174,6 @@ l_Lean_Parser_Tactic_tacticSeq___closed__6 = _init_l_Lean_Parser_Tactic_tacticSe
lean_mark_persistent(l_Lean_Parser_Tactic_tacticSeq___closed__6);
l_Lean_Parser_Tactic_tacticSeq = _init_l_Lean_Parser_Tactic_tacticSeq();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticSeq);
l_Lean_Parser_Tactic_seq1___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___elambda__1___closed__1);
l_Lean_Parser_Tactic_seq1___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___elambda__1___closed__2);
l_Lean_Parser_Tactic_seq1___closed__1 = _init_l_Lean_Parser_Tactic_seq1___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__1);
l_Lean_Parser_Tactic_seq1___closed__2 = _init_l_Lean_Parser_Tactic_seq1___closed__2();
@ -84825,16 +84780,12 @@ lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_return_parenthesizer___clos
res = l___regBuiltin_Lean_Parser_Term_return_parenthesizer(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1);
l_Lean_Parser_Tactic_seq1Unbox___closed__1 = _init_l_Lean_Parser_Tactic_seq1Unbox___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___closed__1);
l_Lean_Parser_Tactic_seq1Unbox___closed__2 = _init_l_Lean_Parser_Tactic_seq1Unbox___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___closed__2);
l_Lean_Parser_Tactic_seq1Unbox___closed__3 = _init_l_Lean_Parser_Tactic_seq1Unbox___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___closed__3);
l_Lean_Parser_Tactic_seq1Unbox___closed__4 = _init_l_Lean_Parser_Tactic_seq1Unbox___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___closed__4);
l_Lean_Parser_Tactic_seq1Unbox = _init_l_Lean_Parser_Tactic_seq1Unbox();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox);
l_Lean_Parser_Tactic_quot___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_quot___elambda__1___closed__1();

57
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c generated
View file

@ -213,6 +213,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_sepBy1_parenthesizer(lean_object
extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__34;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_categoryParserOfStack_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_getConstInfo___rarg___lambda__1___closed__5;
extern lean_object* l_Lean_Unhygienic_MonadQuotation___closed__4;
@ -437,6 +438,7 @@ extern lean_object* l_Lean_mkAppStx___closed__2;
lean_object* l___private_Lean_PrettyPrinter_Parenthesizer_1__regTraceClasses(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__1;
lean_object* l_ReaderT_bind___at_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4;
lean_object* l_Lean_Syntax_Traverser_left(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_quotedSymbol_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_symbolNoWs_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -6888,22 +6890,51 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("seq1");
return x_1;
}
}
lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2;
x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
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;
x_5 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__22;
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* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_5 = l_Array_empty___closed__1;
x_6 = lean_array_push(x_5, x_1);
x_7 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__34;
x_8 = lean_array_push(x_6, x_7);
x_9 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_9);
lean_ctor_set(x_10, 1, x_8);
x_11 = lean_alloc_ctor(0, 2, 0);
x_7 = l_Lean_nullKind___closed__2;
x_8 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
x_9 = lean_array_push(x_5, x_8);
x_10 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_4);
return x_11;
lean_ctor_set(x_11, 1, x_9);
x_12 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__22;
x_13 = lean_array_push(x_12, x_11);
x_14 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__34;
x_15 = lean_array_push(x_13, x_14);
x_16 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3;
x_17 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_4);
return x_18;
}
}
lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__2(lean_object* x_1) {
@ -9647,6 +9678,10 @@ l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2
lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2);
l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3 = _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3();
lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3);
l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4 = _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4();
lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4);
l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5 = _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5();
lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5);
l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__1 = _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__1);
l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2 = _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2();