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:05:42 -07:00
parent cb55ffae94
commit 23f7a4b435
6 changed files with 428 additions and 175 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
stage0/src/Lean/Parser/Tactic.lean generated
View file

@ -74,7 +74,6 @@ def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 match
def withIds : Parser := optional (" with " >> many1 ident')
@[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds
def seq1 := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
@[builtinTacticParser] def paren := parser! "(" >> seq1 >> ")"
@[builtinTacticParser] def nestedTactic := tacticSeqBracketed
@[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1

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

@ -28,6 +28,10 @@ def tacticSeqBracketed : Parser :=
parser! "{" >> sepBy tacticParser "; " true >> "}"
def tacticSeq :=
nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented
/- Raw sequence for quotation and grouping -/
def seq1 := parser! sepBy1 tacticParser "; " true
end Tactic
def darrow : Parser := " => "

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

@ -430,6 +430,7 @@ 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;
@ -986,7 +987,6 @@ lean_object* l_Lean_Parser_Command_mixfix___closed__5;
lean_object* l_Lean_Parser_Syntax_cat_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_elab__rules___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_syntaxAbbrev___closed__3;
extern lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__4;
lean_object* l_Lean_Parser_Command_notation_formatter___closed__4;
extern lean_object* l_Lean_Parser_Term_str_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Syntax_notFollowedBy___closed__7;
@ -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__4;
x_24 = l_Lean_Parser_Tactic_seq1Unbox___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);

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

@ -117,6 +117,7 @@ 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;
lean_object* l_Lean_Parser_Tactic_seq1_formatter___closed__3;
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*);
@ -130,6 +131,7 @@ lean_object* l_Lean_Parser_Tactic_matchAlts_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_orelse___closed__1;
lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__6;
lean_object* l___regBuiltin_Lean_Parser_Tactic_orelse_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_underscore___closed__2;
lean_object* l_Lean_Parser_Tactic_location___closed__7;
lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__9;
@ -170,7 +172,6 @@ lean_object* l___regBuiltinParser_Lean_Parser_Tactic_admit(lean_object*);
lean_object* l_Lean_Parser_Tactic_rewriteSeq___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_intro_formatter___closed__5;
lean_object* l_Lean_Parser_Tactic_admit;
extern lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__2;
extern lean_object* l_Lean_Parser_Term_show___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_case_formatter___closed__4;
lean_object* l___regBuiltin_Lean_Parser_Tactic_rewriteSeq_formatter___closed__1;
@ -260,6 +261,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_have_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_change_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Tactic_injection___closed__8;
lean_object* l_Lean_Parser_Tactic_changeWith___closed__5;
extern lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_matchAlts___closed__1;
lean_object* l_Lean_Parser_Tactic_paren_parenthesizer___closed__2;
lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
@ -333,7 +335,7 @@ lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__3;
lean_object* l_Lean_Parser_Tactic_location___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_let___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_seq1;
extern lean_object* l_Lean_Parser_Tactic_seq1;
extern lean_object* l_Lean_Parser_Term_subtype_formatter___closed__6;
lean_object* l_Lean_Parser_Tactic_refine_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Tactic_revert_formatter(lean_object*);
@ -385,6 +387,7 @@ lean_object* l_Lean_Parser_Tactic_refine_x21___elambda__1(lean_object*, lean_obj
lean_object* l_Lean_Parser_Tactic_revert___closed__1;
lean_object* l_Lean_Parser_Tactic_location___elambda__1___closed__4;
lean_object* l_Lean_Parser_Tactic_skip___closed__1;
lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_sufficesDecl___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_rwRule_formatter___closed__3;
@ -554,6 +557,7 @@ lean_object* l_Lean_Parser_Tactic_clear___closed__3;
lean_object* l_Lean_Parser_Tactic_cases___elambda__1___closed__8;
lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__3;
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_generalize(lean_object*);
extern lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__3;
extern lean_object* l_Lean_Parser_identNoAntiquot___closed__1;
lean_object* l_Lean_Parser_Tactic_intros___closed__8;
lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__3;
@ -734,7 +738,6 @@ 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*);
@ -971,7 +974,6 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_intros_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_apply;
extern lean_object* l_Lean_Parser_antiquotNestedExpr_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_rwRuleSeq_formatter___closed__2;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_assumption___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Tactic_orelse_formatter(lean_object*);
lean_object* l_Lean_Parser_Tactic_changeWith_formatter___closed__2;
@ -1328,7 +1330,6 @@ lean_object* l_Lean_Parser_Tactic_show_formatter___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Tactic_revert_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_locationWildcard___elambda__1___closed__5;
lean_object* l_Lean_Parser_Tactic_withAlts_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_seq1___closed__1;
lean_object* l_Lean_Parser_Tactic_intros;
lean_object* l_Lean_Parser_Tactic_rewriteSeq___closed__3;
lean_object* l_Lean_Parser_Tactic_matchAlt_formatter___closed__2;
@ -1460,7 +1461,6 @@ lean_object* l_Lean_Parser_Tactic_ident_x27_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_failIfSuccess___elambda__1___closed__8;
lean_object* l_Lean_Parser_Tactic_refine_x21___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_matchAlts___closed__2;
lean_object* l_Lean_Parser_Tactic_seq1___closed__2;
lean_object* l_Lean_Parser_Tactic_exact_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__7;
lean_object* l_Lean_Parser_Tactic_refine_x21___closed__6;
@ -1701,6 +1701,8 @@ 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_seq1_formatter___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*);
@ -26014,49 +26016,6 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Parser_Tactic_seq1___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
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_seq1Unbox___elambda__1___spec__1(x_5, x_1, x_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;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_seq1___elambda__1), 2, 0);
return x_1;
}
}
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_seq1Unbox___closed__2;
x_2 = l_Lean_Parser_Tactic_seq1___closed__1;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_seq1___closed__2;
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_paren___elambda__1___closed__1() {
_start:
{
@ -26602,6 +26561,21 @@ return x_7;
lean_object* _init_l_Lean_Parser_Tactic_seq1_formatter___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__1;
x_2 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__3;
x_3 = 1;
x_4 = lean_box(x_3);
x_5 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot_formatter___boxed), 8, 3);
lean_closure_set(x_5, 0, x_1);
lean_closure_set(x_5, 1, x_2);
lean_closure_set(x_5, 2, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__4;
x_2 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__3;
@ -26611,13 +26585,27 @@ lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_seq1_formatter___closed__2;
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);
lean_closure_set(x_4, 2, x_3);
return x_4;
}
}
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);
x_6 = l_Lean_Parser_Tactic_seq1_formatter___closed__1;
x_7 = l_Lean_Parser_Tactic_seq1_formatter___closed__3;
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;
}
}
@ -26714,6 +26702,19 @@ return x_5;
lean_object* _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__3;
x_2 = 1;
x_3 = lean_box(x_2);
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot_parenthesizer___rarg___boxed), 7, 2);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2() {
_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;
@ -26723,13 +26724,27 @@ lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2;
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);
lean_closure_set(x_4, 2, x_3);
return x_4;
}
}
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);
x_6 = l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1;
x_7 = l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3;
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;
}
}
@ -32194,12 +32209,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_injection_parenthesizer__
res = l___regBuiltin_Lean_Parser_Tactic_injection_parenthesizer(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
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();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__2);
l_Lean_Parser_Tactic_seq1 = _init_l_Lean_Parser_Tactic_seq1();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1);
l_Lean_Parser_Tactic_paren___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_paren___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_paren___elambda__1___closed__1);
l_Lean_Parser_Tactic_paren___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_paren___elambda__1___closed__2();
@ -32225,6 +32234,10 @@ 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_seq1_formatter___closed__2 = _init_l_Lean_Parser_Tactic_seq1_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1_formatter___closed__2);
l_Lean_Parser_Tactic_seq1_formatter___closed__3 = _init_l_Lean_Parser_Tactic_seq1_formatter___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1_formatter___closed__3);
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();
@ -32242,6 +32255,10 @@ 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_seq1_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2);
l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3 = _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3);
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();

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

@ -36,6 +36,7 @@ lean_object* l_Lean_Parser_Term_nativeDecide___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_sufficesDecl_formatter___closed__1;
lean_object* l_Lean_Parser_Term_letDecl_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_tupleTail_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Tactic_seq1___closed__3;
lean_object* l_Lean_Parser_Term_matchAlt___closed__5;
lean_object* l_Lean_Parser_Term_instBinder_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_subtype_parenthesizer___closed__6;
@ -292,6 +293,7 @@ lean_object* l_Lean_Parser_Term_bracketedBinder(uint8_t);
lean_object* l_Lean_Parser_Term_structInstLVal_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Term_structInst___closed__6;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_sepBy_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Term_unreachable_parenthesizer(lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Tactic_quot_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Term_explicitUniv_formatter___closed__1;
@ -340,6 +342,7 @@ lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_formatter___closed__1;
lean_object* l_Lean_Parser_Term_ellipsis_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_match_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__4;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__3;
lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__2___closed__2;
@ -618,10 +621,10 @@ lean_object* l_Lean_Parser_Term_infixR_parenthesizer___rarg(lean_object*, lean_o
lean_object* l_Lean_Parser_Term_simpleBinder_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_attrInstance___closed__7;
lean_object* l_Lean_Parser_Term_bracketedBinder_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1___boxed(lean_object*, lean_object*, 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;
@ -782,6 +785,7 @@ lean_object* l_Lean_Parser_Term_matchAlt_formatter(lean_object*, lean_object*, l
lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__3;
lean_object* l_Lean_Parser_Term_matchAlt___closed__7;
lean_object* l_Lean_Parser_Term_syntheticHole_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_seq1;
lean_object* l_Lean_Parser_Term_suffices___closed__8;
lean_object* l_Lean_Parser_Term_subtype_formatter___closed__6;
lean_object* l_Lean_Parser_Term_app___elambda__1(lean_object*, lean_object*);
@ -963,6 +967,7 @@ lean_object* l_Lean_Parser_mkAntiquot_formatter___boxed(lean_object*, lean_objec
lean_object* l_Lean_Parser_leadingNode_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_forall_parenthesizer___closed__8;
lean_object* l_Lean_Parser_Term_let_x21_formatter___closed__3;
lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_matchAlts_formatter___closed__7;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_fun___elambda__1___spec__1(lean_object*, lean_object*);
@ -1319,6 +1324,7 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_forall___elambda
lean_object* l_Lean_Parser_Term_mapRev_formatter___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_iff_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Term_listLit_formatter___closed__2;
lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__3;
lean_object* l___regBuiltinParser_Lean_Parser_Term_parser_x21(lean_object*);
lean_object* l_Lean_Parser_Term_subtype_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_fromTerm___closed__1;
@ -1350,6 +1356,7 @@ lean_object* l_Lean_Parser_Term_letrec___closed__2;
lean_object* l_Lean_Parser_Term_return___closed__6;
lean_object* l_Lean_Parser_Term_letIdLhs___closed__5;
lean_object* l_Lean_Parser_Term_byTactic___elambda__1___closed__8;
lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1;
lean_object* l_Lean_Parser_Level_quot___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_dbgTrace;
lean_object* l_Lean_Parser_Term_match_parenthesizer___closed__2;
@ -1452,7 +1459,6 @@ lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser
extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__7;
lean_object* l___regBuiltin_Lean_Parser_Term_dollarProj_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Term_fromTerm___closed__2;
lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__5;
lean_object* l_Lean_Parser_symbolFn___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Term_funBinder_quot_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_type___elambda__1___closed__5;
@ -1725,6 +1731,7 @@ extern lean_object* l_Lean_strLitKind___closed__1;
lean_object* l_Lean_Parser_Term_unreachable___closed__5;
lean_object* l_Lean_PrettyPrinter_Formatter_toggleInsideQuot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_seq_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_seq1___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_paren_formatter___closed__1;
lean_object* l_Lean_Parser_Term_structInst_formatter___closed__1;
lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__1;
@ -1746,7 +1753,6 @@ 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;
@ -2022,6 +2028,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_symbol_formatter(lean_object*, lean_
lean_object* l_Lean_Parser_Tactic_quot___closed__6;
lean_object* l_Lean_Parser_Term_ne___closed__2;
lean_object* l_Lean_Parser_Term_have_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Tactic_seq1___closed__5;
lean_object* l_Lean_Parser_Term_fcomp___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_type_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_binderDefault___elambda__1___closed__3;
@ -2326,7 +2333,6 @@ lean_object* l_Lean_Parser_Term_sort_formatter___closed__2;
lean_object* l___regBuiltin_Lean_Parser_Term_and_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_instBinder_formatter___closed__4;
lean_object* l_Lean_Parser_Term_not___elambda__1___closed__8;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_match__syntax___closed__4;
lean_object* l_Lean_Parser_Term_ellipsis___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_show___closed__7;
@ -2625,6 +2631,7 @@ lean_object* l_Lean_Parser_Term_infixR(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_let_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_seqLeft___closed__3;
lean_object* l_Lean_Parser_Term_band_formatter___closed__1;
lean_object* l_Lean_Parser_Tactic_seq1___closed__4;
lean_object* l_Lean_Parser_Term_forall_formatter___closed__6;
lean_object* l_Lean_Parser_charLit___elambda__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_letrec___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3220,6 +3227,7 @@ lean_object* l_Lean_Parser_Term_fun_parenthesizer___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Term_cdot_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_explicit_formatter___closed__3;
lean_object* l_Lean_Parser_Term_not___closed__1;
lean_object* l_Lean_Parser_Tactic_seq1___closed__1;
lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Level_quot_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Term_uminus___closed__1;
@ -3446,6 +3454,7 @@ lean_object* l_Lean_Parser_Term_structInstField_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_fcomp___closed__3;
lean_object* l_Lean_Parser_Term_sort_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_attrInstance_parenthesizer___closed__5;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_anonymousCtor_parenthesizer___closed__2;
extern lean_object* l_Lean_mkHole___closed__2;
lean_object* l_Lean_Parser_Term_type___closed__5;
@ -3553,6 +3562,7 @@ lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser
lean_object* l_Lean_Parser_Term_bor___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_attrInstance___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_hole___closed__3;
lean_object* l_Lean_Parser_Tactic_seq1___closed__2;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_explicitBinder_formatter___closed__7;
lean_object* l_Lean_Parser_Term_byTactic___closed__6;
@ -3761,6 +3771,7 @@ lean_object* l_Lean_Parser_Term_matchAlts_formatter(uint8_t, lean_object*, lean_
lean_object* l_Lean_Parser_Term_binderTactic_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Level_quot_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_matchDiscr___closed__9;
lean_object* l_Lean_Parser_Tactic_seq1___closed__6;
lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_proj___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_sort_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3822,7 +3833,6 @@ lean_object* l_Lean_Parser_Term_syntheticHole_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_show_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_parenSpecial_formatter___closed__3;
lean_object* l_Lean_Parser_Term_bne___elambda__1___closed__1;
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4;
lean_object* l_Lean_Parser_Term_dollar___closed__1;
lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_match_formatter(lean_object*);
@ -4095,6 +4105,7 @@ 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*);
@ -4514,6 +4525,24 @@ x_7 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic
return x_7;
}
}
lean_object* _init_l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("seq");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_tacticSeq1Indented___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_tacticSeq1Indented___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -4540,7 +4569,7 @@ lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_1, 4, x_11);
x_12 = 0;
x_13 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__1(x_12, x_1, x_2);
x_14 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_14 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2;
x_15 = l_Lean_Parser_ParserState_mkNode(x_13, x_14, x_4);
return x_15;
}
@ -4574,7 +4603,7 @@ lean_ctor_set(x_25, 4, x_24);
lean_ctor_set_uint8(x_25, sizeof(void*)*5, x_20);
x_26 = 0;
x_27 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__1(x_26, x_25, x_2);
x_28 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_28 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2;
x_29 = l_Lean_Parser_ParserState_mkNode(x_27, x_28, x_4);
return x_29;
}
@ -4625,7 +4654,7 @@ lean_object* _init_l_Lean_Parser_Tactic_tacticSeq1Indented___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__5;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2;
x_2 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__4;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -5600,6 +5629,256 @@ x_1 = l_Lean_Parser_Tactic_tacticSeq___closed__6;
return x_1;
}
}
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object* x_7;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_array_get_size(x_4);
lean_dec(x_4);
x_6 = 0;
x_7 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1___spec__2(x_1, x_5, x_6, x_2, x_3);
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* _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__1;
x_2 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__3;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_Parser_Tactic_seq1___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__4;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_inc(x_2);
lean_inc(x_1);
x_5 = l_Lean_Parser_tryAnti(x_1, x_2);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
lean_dec(x_4);
x_6 = lean_unsigned_to_nat(1024u);
x_7 = l_Lean_Parser_checkPrecFn(x_6, x_1, x_2);
x_8 = lean_ctor_get(x_7, 3);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = lean_ctor_get(x_7, 0);
lean_inc(x_9);
x_10 = lean_array_get_size(x_9);
lean_dec(x_9);
x_11 = 1;
x_12 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(x_11, x_1, x_7);
x_13 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
x_14 = l_Lean_Parser_ParserState_mkNode(x_12, x_13, x_10);
return x_14;
}
else
{
lean_dec(x_8);
lean_dec(x_1);
return x_7;
}
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_15 = lean_ctor_get(x_2, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
x_17 = lean_ctor_get(x_2, 1);
lean_inc(x_17);
lean_inc(x_1);
x_18 = lean_apply_2(x_4, x_1, x_2);
x_19 = lean_ctor_get(x_18, 3);
lean_inc(x_19);
if (lean_obj_tag(x_19) == 0)
{
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_1);
return x_18;
}
else
{
lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
lean_dec(x_19);
x_21 = lean_ctor_get(x_18, 1);
lean_inc(x_21);
x_22 = lean_nat_dec_eq(x_21, x_17);
lean_dec(x_21);
if (x_22 == 0)
{
lean_dec(x_20);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_1);
return x_18;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_inc(x_17);
x_23 = l_Lean_Parser_ParserState_restore(x_18, x_16, x_17);
lean_dec(x_16);
x_24 = lean_unsigned_to_nat(1024u);
x_25 = l_Lean_Parser_checkPrecFn(x_24, x_1, x_23);
x_26 = lean_ctor_get(x_25, 3);
lean_inc(x_26);
if (lean_obj_tag(x_26) == 0)
{
lean_object* x_27; lean_object* x_28; uint8_t x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_27 = lean_ctor_get(x_25, 0);
lean_inc(x_27);
x_28 = lean_array_get_size(x_27);
lean_dec(x_27);
x_29 = 1;
x_30 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(x_29, x_1, x_25);
x_31 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2;
x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_28);
x_33 = l_Lean_Parser_mergeOrElseErrors(x_32, x_20, x_17, x_29);
lean_dec(x_17);
return x_33;
}
else
{
uint8_t x_34; lean_object* x_35;
lean_dec(x_26);
lean_dec(x_1);
x_34 = 1;
x_35 = l_Lean_Parser_mergeOrElseErrors(x_25, x_20, x_17, x_34);
lean_dec(x_17);
return x_35;
}
}
}
}
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__1;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2;
x_4 = l_Lean_Parser_sepBy1Info(x_2, x_3);
return x_4;
}
}
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_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_seq1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_seq1___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_seq1___closed__3;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_seq1___elambda__1), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_seq1___closed__4;
x_2 = l_Lean_Parser_Tactic_seq1___closed__5;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_seq1___closed__6;
return x_1;
}
}
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(x_4, x_2, x_3);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_darrow___elambda__1___closed__1() {
_start:
{
@ -6703,7 +6982,7 @@ lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_formatter(lean_object* x_1,
_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_6 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2;
x_7 = l_Lean_Parser_Tactic_tacticSeq1Indented_formatter___closed__5;
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;
@ -7020,7 +7299,7 @@ lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer(lean_object*
_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_6 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2;
x_7 = l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer___closed__5;
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;
@ -70968,7 +71247,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4;
x_2 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -75841,19 +76120,6 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object* x_7;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_array_get_size(x_4);
lean_dec(x_4);
x_6 = 0;
x_7 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1___spec__2(x_1, x_5, x_6, x_2, x_3);
return x_7;
}
}
lean_object* l_Lean_Parser_Tactic_seq1Unbox___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -75863,8 +76129,8 @@ lean_inc(x_3);
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_seq1Unbox___elambda__1___spec__1(x_5, x_1, x_2);
x_7 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
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_tacticSeq1Indented___elambda__1___closed__2;
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);
@ -75909,35 +76175,23 @@ 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; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__1;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2;
x_4 = l_Lean_Parser_sepBy1Info(x_2, x_3);
return x_4;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2;
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; lean_object* x_3;
x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_2 = l_Lean_Parser_Tactic_seq1Unbox___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__2;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__1;
x_2 = l_Lean_Parser_withResultOfInfo(x_1);
return x_2;
}
}
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;
@ -75945,12 +76199,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__5() {
lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__3;
x_2 = l_Lean_Parser_Tactic_seq1Unbox___closed__4;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__2;
x_2 = l_Lean_Parser_Tactic_seq1Unbox___closed__3;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -75961,20 +76215,10 @@ lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__5;
x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__4;
return x_1;
}
}
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1(x_4, x_2, x_3);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Tactic_quot___elambda__1___closed__1() {
_start:
{
@ -76144,7 +76388,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__4;
x_13 = l_Lean_Parser_Tactic_seq1Unbox___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);
@ -76360,7 +76604,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__4;
x_73 = l_Lean_Parser_Tactic_seq1Unbox___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);
@ -76579,7 +76823,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_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_6 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2;
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);
@ -76700,7 +76944,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_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5;
x_6 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2;
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);
@ -77650,6 +77894,10 @@ l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacti
lean_mark_persistent(l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__2___closed__4);
l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__2___closed__5 = _init_l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__2___closed__5();
lean_mark_persistent(l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__2___closed__5);
l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1);
l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2);
l_Lean_Parser_Tactic_tacticSeq1Indented___closed__1 = _init_l_Lean_Parser_Tactic_tacticSeq1Indented___closed__1();
lean_mark_persistent(l_Lean_Parser_Tactic_tacticSeq1Indented___closed__1);
l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2 = _init_l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2();
@ -77726,6 +77974,28 @@ 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___elambda__1___closed__3 = _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___elambda__1___closed__3);
l_Lean_Parser_Tactic_seq1___elambda__1___closed__4 = _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___elambda__1___closed__4);
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();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__2);
l_Lean_Parser_Tactic_seq1___closed__3 = _init_l_Lean_Parser_Tactic_seq1___closed__3();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__3);
l_Lean_Parser_Tactic_seq1___closed__4 = _init_l_Lean_Parser_Tactic_seq1___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__4);
l_Lean_Parser_Tactic_seq1___closed__5 = _init_l_Lean_Parser_Tactic_seq1___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__5);
l_Lean_Parser_Tactic_seq1___closed__6 = _init_l_Lean_Parser_Tactic_seq1___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__6);
l_Lean_Parser_Tactic_seq1 = _init_l_Lean_Parser_Tactic_seq1();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1);
l_Lean_Parser_darrow___elambda__1___closed__1 = _init_l_Lean_Parser_darrow___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_darrow___elambda__1___closed__1);
l_Lean_Parser_darrow___elambda__1___closed__2 = _init_l_Lean_Parser_darrow___elambda__1___closed__2();
@ -84320,8 +84590,6 @@ l_Lean_Parser_Tactic_seq1Unbox___closed__3 = _init_l_Lean_Parser_Tactic_seq1Unbo
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___closed__5 = _init_l_Lean_Parser_Tactic_seq1Unbox___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___closed__5);
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,7 +213,6 @@ 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;
@ -438,7 +437,6 @@ 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*);
@ -6890,51 +6888,22 @@ 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("seq");
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; 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;
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;
x_6 = lean_array_push(x_5, x_1);
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);
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);
lean_ctor_set(x_11, 0, x_10);
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_ctor_set(x_11, 1, x_4);
return x_11;
}
}
lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__2(lean_object* x_1) {
@ -9678,10 +9647,6 @@ 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();