chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
e1ad5a948b
commit
489da27208
9 changed files with 1429 additions and 540 deletions
1
stage0/src/Lean/Parser/Tactic.lean
generated
1
stage0/src/Lean/Parser/Tactic.lean
generated
|
|
@ -37,6 +37,7 @@ def ident' : Parser := ident <|> underscore
|
|||
@[builtinTacticParser] def «refine!» := parser! nonReservedSymbol "refine! " >> termParser
|
||||
@[builtinTacticParser] def «case» := parser! nonReservedSymbol "case " >> ident >> darrow >> tacticSeq
|
||||
@[builtinTacticParser] def «allGoals» := parser! nonReservedSymbol "allGoals " >> tacticSeq
|
||||
@[builtinTacticParser] def «focus» := parser! nonReservedSymbol "focus " >> tacticSeq
|
||||
@[builtinTacticParser] def «skip» := parser! nonReservedSymbol "skip"
|
||||
@[builtinTacticParser] def «done» := parser! nonReservedSymbol "done"
|
||||
@[builtinTacticParser] def «admit» := parser! nonReservedSymbol "admit"
|
||||
|
|
|
|||
32
stage0/stdlib/Lean/Delaborator.c
generated
32
stage0/stdlib/Lean/Delaborator.c
generated
|
|
@ -385,6 +385,7 @@ lean_object* l_Lean_Delaborator_delabDiv___lambda__1___boxed(lean_object*, lean_
|
|||
lean_object* l_Lean_Delaborator_delabOrM___lambda__1___closed__1;
|
||||
lean_object* l___regBuiltin_Lean_Delaborator_delabBAnd___closed__1;
|
||||
lean_object* l___regBuiltin_Lean_Delaborator_delabOr___closed__2;
|
||||
lean_object* l_Lean_Delaborator_delabLetE___closed__16;
|
||||
lean_object* l_Lean_Delaborator_delabStructureInstance___lambda__1___closed__3;
|
||||
lean_object* l_Lean_Delaborator_delabInfixOp___lambda__2___closed__1;
|
||||
lean_object* l___regBuiltin_Lean_Delaborator_delabCoe___closed__2;
|
||||
|
|
@ -621,6 +622,7 @@ lean_object* l_Array_umapMAux___main___at_Lean_Delaborator_delabConst___spec__1(
|
|||
lean_object* l_Lean_mkSepArray(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Delaborator_delabProjectionApp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_redLength___main___rarg(lean_object*);
|
||||
lean_object* l_Lean_Delaborator_delabLetE___closed__15;
|
||||
lean_object* l___private_Lean_Delaborator_2__unresolveUsingNamespace___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Delaborator_mkDelabAttribute___closed__4;
|
||||
lean_object* l___regBuiltin_Lean_Delaborator_delabGE___closed__1;
|
||||
|
|
@ -16563,6 +16565,28 @@ lean_ctor_set(x_3, 1, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabLetE___closed__15() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Array_empty___closed__1;
|
||||
x_2 = l_Lean_Delaborator_delabLetE___closed__14;
|
||||
x_3 = lean_array_push(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Delaborator_delabLetE___closed__16() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_nullKind___closed__2;
|
||||
x_2 = l_Lean_Delaborator_delabLetE___closed__15;
|
||||
x_3 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Delaborator_delabLetE(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -16664,7 +16688,7 @@ lean_ctor_set(x_49, 0, x_48);
|
|||
lean_ctor_set(x_49, 1, x_47);
|
||||
x_50 = l_Lean_Delaborator_delabLetE___closed__4;
|
||||
x_51 = lean_array_push(x_50, x_49);
|
||||
x_52 = l_Lean_Delaborator_delabLetE___closed__14;
|
||||
x_52 = l_Lean_Delaborator_delabLetE___closed__16;
|
||||
x_53 = lean_array_push(x_51, x_52);
|
||||
x_54 = lean_array_push(x_53, x_28);
|
||||
x_55 = l_Lean_Delaborator_delabLetE___closed__2;
|
||||
|
|
@ -16713,7 +16737,7 @@ lean_ctor_set(x_79, 0, x_78);
|
|||
lean_ctor_set(x_79, 1, x_77);
|
||||
x_80 = l_Lean_Delaborator_delabLetE___closed__4;
|
||||
x_81 = lean_array_push(x_80, x_79);
|
||||
x_82 = l_Lean_Delaborator_delabLetE___closed__14;
|
||||
x_82 = l_Lean_Delaborator_delabLetE___closed__16;
|
||||
x_83 = lean_array_push(x_81, x_82);
|
||||
x_84 = lean_array_push(x_83, x_57);
|
||||
x_85 = l_Lean_Delaborator_delabLetE___closed__2;
|
||||
|
|
@ -25479,6 +25503,10 @@ l_Lean_Delaborator_delabLetE___closed__13 = _init_l_Lean_Delaborator_delabLetE__
|
|||
lean_mark_persistent(l_Lean_Delaborator_delabLetE___closed__13);
|
||||
l_Lean_Delaborator_delabLetE___closed__14 = _init_l_Lean_Delaborator_delabLetE___closed__14();
|
||||
lean_mark_persistent(l_Lean_Delaborator_delabLetE___closed__14);
|
||||
l_Lean_Delaborator_delabLetE___closed__15 = _init_l_Lean_Delaborator_delabLetE___closed__15();
|
||||
lean_mark_persistent(l_Lean_Delaborator_delabLetE___closed__15);
|
||||
l_Lean_Delaborator_delabLetE___closed__16 = _init_l_Lean_Delaborator_delabLetE___closed__16();
|
||||
lean_mark_persistent(l_Lean_Delaborator_delabLetE___closed__16);
|
||||
l___regBuiltin_Lean_Delaborator_delabLetE___closed__1 = _init_l___regBuiltin_Lean_Delaborator_delabLetE___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLetE___closed__1);
|
||||
res = l___regBuiltin_Lean_Delaborator_delabLetE(lean_io_mk_world());
|
||||
|
|
|
|||
3
stage0/stdlib/Lean/Elab/Binders.c
generated
3
stage0/stdlib/Lean/Elab/Binders.c
generated
|
|
@ -18,6 +18,7 @@ lean_object* l___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux___mai
|
|||
lean_object* l_Lean_Syntax_updateKind(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabBinder___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabBinders(lean_object*);
|
||||
extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
lean_object* l___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__12;
|
||||
lean_object* l___private_Lean_Elab_Binders_2__expandBinderIdent(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -16908,7 +16909,7 @@ lean_ctor_set(x_121, 0, x_120);
|
|||
lean_ctor_set(x_121, 1, x_119);
|
||||
x_122 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_123 = lean_array_push(x_122, x_121);
|
||||
x_124 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_124 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_125 = lean_array_push(x_123, x_124);
|
||||
x_126 = l___private_Lean_Elab_Binders_11__expandFunBindersAux___main___closed__7;
|
||||
x_127 = lean_array_push(x_126, x_102);
|
||||
|
|
|
|||
1259
stage0/stdlib/Lean/Elab/BuiltinNotation.c
generated
1259
stage0/stdlib/Lean/Elab/BuiltinNotation.c
generated
File diff suppressed because it is too large
Load diff
9
stage0/stdlib/Lean/Elab/Do.c
generated
9
stage0/stdlib/Lean/Elab/Do.c
generated
|
|
@ -14,6 +14,7 @@
|
|||
extern "C" {
|
||||
#endif
|
||||
extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__15;
|
||||
extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
lean_object* l___private_Lean_Elab_Do_6__expandLiftMethodAux___main___closed__4;
|
||||
lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Do_11__processDoElemsAux___main___closed__4;
|
||||
|
|
@ -3478,7 +3479,7 @@ lean_ctor_set(x_492, 0, x_491);
|
|||
lean_ctor_set(x_492, 1, x_490);
|
||||
x_493 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_494 = lean_array_push(x_493, x_472);
|
||||
x_495 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_495 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_496 = lean_array_push(x_494, x_495);
|
||||
x_497 = lean_array_push(x_496, x_492);
|
||||
x_498 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -3535,7 +3536,7 @@ x_517 = l_Lean_Syntax_getArg(x_516, x_515);
|
|||
lean_dec(x_516);
|
||||
x_518 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_519 = lean_array_push(x_518, x_472);
|
||||
x_520 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_520 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_521 = lean_array_push(x_519, x_520);
|
||||
x_522 = lean_array_push(x_521, x_517);
|
||||
x_523 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -4363,7 +4364,7 @@ lean_ctor_set(x_980, 0, x_979);
|
|||
lean_ctor_set(x_980, 1, x_978);
|
||||
x_981 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_982 = lean_array_push(x_981, x_960);
|
||||
x_983 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_983 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_984 = lean_array_push(x_982, x_983);
|
||||
x_985 = lean_array_push(x_984, x_980);
|
||||
x_986 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -4425,7 +4426,7 @@ x_1007 = l_Lean_Syntax_getArg(x_1006, x_1005);
|
|||
lean_dec(x_1006);
|
||||
x_1008 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_1009 = lean_array_push(x_1008, x_960);
|
||||
x_1010 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_1010 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_1011 = lean_array_push(x_1009, x_1010);
|
||||
x_1012 = lean_array_push(x_1011, x_1007);
|
||||
x_1013 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
|
|||
6
stage0/stdlib/Lean/Elab/Match.c
generated
6
stage0/stdlib/Lean/Elab/Match.c
generated
|
|
@ -19,6 +19,7 @@ lean_object* l_List_reverse___rarg(lean_object*);
|
|||
lean_object* l___private_Lean_Elab_Match_9__getMatchAlts(lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabInaccessible___closed__2;
|
||||
lean_object* l___private_Lean_Elab_Match_27__nameToPattern___main___closed__3;
|
||||
extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabNoMatch___closed__1;
|
||||
lean_object* l_Lean_mkAppStx(lean_object*, lean_object*);
|
||||
|
|
@ -427,7 +428,6 @@ extern lean_object* l___private_Lean_Elab_App_22__elabAppFn___main___closed__5;
|
|||
uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_elabMatch___spec__10(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Match_3__elabDiscrsWitMatchTypeAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
lean_object* l_Lean_Elab_Term_elabMVarWithIdKind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Match_6__elabMatchTypeAndDiscrsAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -741,7 +741,7 @@ lean_ctor_set(x_29, 0, x_28);
|
|||
lean_ctor_set(x_29, 1, x_27);
|
||||
x_30 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_31 = lean_array_push(x_30, x_29);
|
||||
x_32 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_32 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_33 = lean_array_push(x_31, x_32);
|
||||
x_34 = lean_array_push(x_33, x_4);
|
||||
x_35 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -853,7 +853,7 @@ lean_ctor_set(x_37, 0, x_36);
|
|||
lean_ctor_set(x_37, 1, x_35);
|
||||
x_38 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_39 = lean_array_push(x_38, x_37);
|
||||
x_40 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_40 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_41 = lean_array_push(x_39, x_40);
|
||||
x_42 = lean_array_push(x_41, x_5);
|
||||
x_43 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
|
|||
90
stage0/stdlib/Lean/Elab/Quotation.c
generated
90
stage0/stdlib/Lean/Elab/Quotation.c
generated
|
|
@ -18,6 +18,7 @@ uint8_t l_Lean_Syntax_isQuot(lean_object*);
|
|||
extern lean_object* l_Lean_Expr_eq_x3f___closed__1;
|
||||
lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__15;
|
||||
lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__56;
|
||||
lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
lean_object* l_List_foldl___main___at___private_Lean_Elab_Quotation_10__toPreterm___main___spec__3(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Quotation_9__exprPlaceholder___closed__1;
|
||||
lean_object* l___private_Lean_Elab_Quotation_8__letBindRhss___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -133,6 +134,7 @@ lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__1;
|
|||
lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSyntax___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_Quotation_antiquotKind_x3f___closed__1;
|
||||
lean_object* l_List_head_x21___at___private_Lean_Elab_Quotation_6__compileStxMatch___main___spec__2___closed__3;
|
||||
lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17;
|
||||
lean_object* lean_string_utf8_byte_size(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_Quotation_elabStxQuot(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_mkAppStx___closed__4;
|
||||
|
|
@ -4670,6 +4672,28 @@ lean_ctor_set(x_3, 1, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Array_empty___closed__1;
|
||||
x_2 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_3 = lean_array_push(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_nullKind___closed__2;
|
||||
x_2 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17;
|
||||
x_3 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3(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) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -4715,7 +4739,7 @@ lean_ctor_set(x_34, 0, x_33);
|
|||
lean_ctor_set(x_34, 1, x_32);
|
||||
x_35 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_36 = lean_array_push(x_35, x_34);
|
||||
x_37 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_37 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_38 = lean_array_push(x_36, x_37);
|
||||
x_39 = lean_array_push(x_38, x_2);
|
||||
x_40 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -4762,7 +4786,7 @@ lean_ctor_set(x_62, 0, x_61);
|
|||
lean_ctor_set(x_62, 1, x_60);
|
||||
x_63 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_64 = lean_array_push(x_63, x_62);
|
||||
x_65 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_65 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_66 = lean_array_push(x_64, x_65);
|
||||
x_67 = lean_array_push(x_66, x_2);
|
||||
x_68 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -5051,7 +5075,7 @@ lean_ctor_set(x_58, 0, x_21);
|
|||
lean_ctor_set(x_58, 1, x_57);
|
||||
x_59 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_60 = lean_array_push(x_59, x_58);
|
||||
x_61 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_61 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_62 = lean_array_push(x_60, x_61);
|
||||
x_63 = lean_array_push(x_62, x_4);
|
||||
x_64 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -5136,7 +5160,7 @@ lean_ctor_set(x_107, 0, x_70);
|
|||
lean_ctor_set(x_107, 1, x_106);
|
||||
x_108 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_109 = lean_array_push(x_108, x_107);
|
||||
x_110 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_110 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_111 = lean_array_push(x_109, x_110);
|
||||
x_112 = lean_array_push(x_111, x_4);
|
||||
x_113 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -5255,7 +5279,7 @@ lean_ctor_set(x_34, 0, x_33);
|
|||
lean_ctor_set(x_34, 1, x_32);
|
||||
x_35 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_36 = lean_array_push(x_35, x_34);
|
||||
x_37 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_37 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_38 = lean_array_push(x_36, x_37);
|
||||
x_39 = lean_array_push(x_38, x_2);
|
||||
x_40 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -5302,7 +5326,7 @@ lean_ctor_set(x_62, 0, x_61);
|
|||
lean_ctor_set(x_62, 1, x_60);
|
||||
x_63 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_64 = lean_array_push(x_63, x_62);
|
||||
x_65 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_65 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_66 = lean_array_push(x_64, x_65);
|
||||
x_67 = lean_array_push(x_66, x_2);
|
||||
x_68 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -8068,7 +8092,7 @@ lean_ctor_set(x_83, 0, x_82);
|
|||
lean_ctor_set(x_83, 1, x_81);
|
||||
x_84 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_85 = lean_array_push(x_84, x_83);
|
||||
x_86 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_86 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_87 = lean_array_push(x_85, x_86);
|
||||
x_88 = lean_array_push(x_87, x_58);
|
||||
x_89 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -8114,7 +8138,7 @@ lean_ctor_set(x_110, 0, x_109);
|
|||
lean_ctor_set(x_110, 1, x_108);
|
||||
x_111 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_112 = lean_array_push(x_111, x_110);
|
||||
x_113 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_113 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_114 = lean_array_push(x_112, x_113);
|
||||
x_115 = lean_array_push(x_114, x_58);
|
||||
x_116 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -8273,7 +8297,7 @@ lean_ctor_set(x_181, 0, x_180);
|
|||
lean_ctor_set(x_181, 1, x_179);
|
||||
x_182 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_183 = lean_array_push(x_182, x_181);
|
||||
x_184 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_184 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_185 = lean_array_push(x_183, x_184);
|
||||
x_186 = lean_array_push(x_148, x_161);
|
||||
x_187 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19;
|
||||
|
|
@ -8346,7 +8370,7 @@ lean_ctor_set(x_225, 0, x_224);
|
|||
lean_ctor_set(x_225, 1, x_223);
|
||||
x_226 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_227 = lean_array_push(x_226, x_225);
|
||||
x_228 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_228 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_229 = lean_array_push(x_227, x_228);
|
||||
x_230 = lean_array_push(x_148, x_161);
|
||||
x_231 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19;
|
||||
|
|
@ -8564,7 +8588,7 @@ lean_ctor_set(x_317, 0, x_316);
|
|||
lean_ctor_set(x_317, 1, x_315);
|
||||
x_318 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_319 = lean_array_push(x_318, x_317);
|
||||
x_320 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_320 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_321 = lean_array_push(x_319, x_320);
|
||||
x_322 = lean_array_push(x_283, x_296);
|
||||
x_323 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19;
|
||||
|
|
@ -8824,7 +8848,7 @@ lean_ctor_set(x_402, 0, x_401);
|
|||
lean_ctor_set(x_402, 1, x_400);
|
||||
x_403 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_404 = lean_array_push(x_403, x_402);
|
||||
x_405 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_405 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_406 = lean_array_push(x_404, x_405);
|
||||
x_407 = lean_array_push(x_406, x_376);
|
||||
x_408 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -9014,7 +9038,7 @@ lean_ctor_set(x_478, 0, x_477);
|
|||
lean_ctor_set(x_478, 1, x_476);
|
||||
x_479 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_480 = lean_array_push(x_479, x_478);
|
||||
x_481 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_481 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_482 = lean_array_push(x_480, x_481);
|
||||
x_483 = lean_array_push(x_444, x_457);
|
||||
x_484 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19;
|
||||
|
|
@ -9334,7 +9358,7 @@ lean_ctor_set(x_578, 0, x_577);
|
|||
lean_ctor_set(x_578, 1, x_576);
|
||||
x_579 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_580 = lean_array_push(x_579, x_578);
|
||||
x_581 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_581 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_582 = lean_array_push(x_580, x_581);
|
||||
x_583 = lean_array_push(x_582, x_553);
|
||||
x_584 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -9380,7 +9404,7 @@ lean_ctor_set(x_605, 0, x_604);
|
|||
lean_ctor_set(x_605, 1, x_603);
|
||||
x_606 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_607 = lean_array_push(x_606, x_605);
|
||||
x_608 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_608 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_609 = lean_array_push(x_607, x_608);
|
||||
x_610 = lean_array_push(x_609, x_553);
|
||||
x_611 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -9611,7 +9635,7 @@ lean_ctor_set(x_719, 0, x_718);
|
|||
lean_ctor_set(x_719, 1, x_717);
|
||||
x_720 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_721 = lean_array_push(x_720, x_719);
|
||||
x_722 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_722 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_723 = lean_array_push(x_721, x_722);
|
||||
x_724 = lean_array_push(x_643, x_700);
|
||||
x_725 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19;
|
||||
|
|
@ -9683,7 +9707,7 @@ lean_ctor_set(x_762, 0, x_761);
|
|||
lean_ctor_set(x_762, 1, x_760);
|
||||
x_763 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_764 = lean_array_push(x_763, x_762);
|
||||
x_765 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_765 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_766 = lean_array_push(x_764, x_765);
|
||||
x_767 = lean_array_push(x_643, x_700);
|
||||
x_768 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19;
|
||||
|
|
@ -9974,7 +9998,7 @@ lean_ctor_set(x_897, 0, x_896);
|
|||
lean_ctor_set(x_897, 1, x_895);
|
||||
x_898 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_899 = lean_array_push(x_898, x_897);
|
||||
x_900 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_900 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_901 = lean_array_push(x_899, x_900);
|
||||
x_902 = lean_array_push(x_820, x_877);
|
||||
x_903 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19;
|
||||
|
|
@ -10237,7 +10261,7 @@ lean_ctor_set(x_982, 0, x_981);
|
|||
lean_ctor_set(x_982, 1, x_980);
|
||||
x_983 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_984 = lean_array_push(x_983, x_982);
|
||||
x_985 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_985 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_986 = lean_array_push(x_984, x_985);
|
||||
x_987 = lean_array_push(x_986, x_956);
|
||||
x_988 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -10499,7 +10523,7 @@ lean_ctor_set(x_1101, 0, x_1100);
|
|||
lean_ctor_set(x_1101, 1, x_1099);
|
||||
x_1102 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_1103 = lean_array_push(x_1102, x_1101);
|
||||
x_1104 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_1104 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_1105 = lean_array_push(x_1103, x_1104);
|
||||
x_1106 = lean_array_push(x_1024, x_1081);
|
||||
x_1107 = l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__19;
|
||||
|
|
@ -11262,7 +11286,7 @@ lean_ctor_set(x_84, 0, x_83);
|
|||
lean_ctor_set(x_84, 1, x_82);
|
||||
x_85 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_86 = lean_array_push(x_85, x_84);
|
||||
x_87 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_87 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_88 = lean_array_push(x_86, x_87);
|
||||
x_89 = lean_array_push(x_88, x_59);
|
||||
x_90 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -11310,7 +11334,7 @@ lean_ctor_set(x_111, 0, x_110);
|
|||
lean_ctor_set(x_111, 1, x_109);
|
||||
x_112 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_113 = lean_array_push(x_112, x_111);
|
||||
x_114 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_114 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_115 = lean_array_push(x_113, x_114);
|
||||
x_116 = lean_array_push(x_115, x_59);
|
||||
x_117 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -11472,7 +11496,7 @@ lean_ctor_set(x_170, 0, x_169);
|
|||
lean_ctor_set(x_170, 1, x_168);
|
||||
x_171 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_172 = lean_array_push(x_171, x_170);
|
||||
x_173 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_173 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_174 = lean_array_push(x_172, x_173);
|
||||
x_175 = lean_array_push(x_174, x_144);
|
||||
x_176 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -11678,7 +11702,7 @@ lean_ctor_set(x_252, 0, x_251);
|
|||
lean_ctor_set(x_252, 1, x_250);
|
||||
x_253 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_254 = lean_array_push(x_253, x_252);
|
||||
x_255 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_255 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_256 = lean_array_push(x_254, x_255);
|
||||
x_257 = lean_array_push(x_256, x_230);
|
||||
x_258 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -11721,7 +11745,7 @@ lean_ctor_set(x_276, 0, x_275);
|
|||
lean_ctor_set(x_276, 1, x_274);
|
||||
x_277 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_278 = lean_array_push(x_277, x_276);
|
||||
x_279 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_279 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_280 = lean_array_push(x_278, x_279);
|
||||
x_281 = lean_array_push(x_280, x_230);
|
||||
x_282 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -11878,7 +11902,7 @@ lean_ctor_set(x_332, 0, x_331);
|
|||
lean_ctor_set(x_332, 1, x_330);
|
||||
x_333 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_334 = lean_array_push(x_333, x_332);
|
||||
x_335 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_335 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_336 = lean_array_push(x_334, x_335);
|
||||
x_337 = lean_array_push(x_336, x_309);
|
||||
x_338 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -12100,7 +12124,7 @@ lean_ctor_set(x_414, 0, x_413);
|
|||
lean_ctor_set(x_414, 1, x_412);
|
||||
x_415 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_416 = lean_array_push(x_415, x_414);
|
||||
x_417 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_417 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_418 = lean_array_push(x_416, x_417);
|
||||
x_419 = lean_array_push(x_418, x_391);
|
||||
x_420 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -12335,7 +12359,7 @@ lean_ctor_set(x_501, 0, x_500);
|
|||
lean_ctor_set(x_501, 1, x_499);
|
||||
x_502 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_503 = lean_array_push(x_502, x_501);
|
||||
x_504 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_504 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_505 = lean_array_push(x_503, x_504);
|
||||
x_506 = lean_array_push(x_505, x_475);
|
||||
x_507 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -12575,7 +12599,7 @@ lean_ctor_set(x_588, 0, x_587);
|
|||
lean_ctor_set(x_588, 1, x_586);
|
||||
x_589 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_590 = lean_array_push(x_589, x_588);
|
||||
x_591 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_591 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_592 = lean_array_push(x_590, x_591);
|
||||
x_593 = lean_array_push(x_592, x_565);
|
||||
x_594 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -12826,7 +12850,7 @@ lean_ctor_set(x_678, 0, x_677);
|
|||
lean_ctor_set(x_678, 1, x_676);
|
||||
x_679 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_680 = lean_array_push(x_679, x_678);
|
||||
x_681 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_681 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_682 = lean_array_push(x_680, x_681);
|
||||
x_683 = lean_array_push(x_682, x_652);
|
||||
x_684 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -13069,7 +13093,7 @@ lean_ctor_set(x_765, 0, x_764);
|
|||
lean_ctor_set(x_765, 1, x_763);
|
||||
x_766 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_767 = lean_array_push(x_766, x_765);
|
||||
x_768 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_768 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_769 = lean_array_push(x_767, x_768);
|
||||
x_770 = lean_array_push(x_769, x_742);
|
||||
x_771 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -23860,6 +23884,10 @@ l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__15 = _init
|
|||
lean_mark_persistent(l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__15);
|
||||
l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16 = _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16();
|
||||
lean_mark_persistent(l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16);
|
||||
l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17 = _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17();
|
||||
lean_mark_persistent(l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__17);
|
||||
l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18 = _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18();
|
||||
lean_mark_persistent(l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18);
|
||||
l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___closed__1 = _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___closed__1();
|
||||
lean_mark_persistent(l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___closed__1);
|
||||
l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___closed__2 = _init_l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___closed__2();
|
||||
|
|
|
|||
10
stage0/stdlib/Lean/Elab/StructInst.c
generated
10
stage0/stdlib/Lean/Elab/StructInst.c
generated
|
|
@ -19,6 +19,7 @@ lean_object* l_Lean_Elab_Term_StructInst_formatStruct___main(lean_object*);
|
|||
lean_object* l___private_Lean_Elab_StructInst_1__expandNonAtomicExplicitSource___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_StructInst_Struct_modifyFields(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_fmt___at_Lean_Position_Lean_HasFormat___spec__1(lean_object*);
|
||||
extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
lean_object* l_List_forM___main___at_Lean_Elab_Term_StructInst_DefaultFields_step___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_StructInst_17__groupFields___lambda__2___boxed(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_StructInst_12__mkFieldMap(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -372,7 +373,6 @@ extern lean_object* l_Lean_Syntax_inhabited;
|
|||
size_t lean_ptr_addr(lean_object*);
|
||||
lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_StructInst_3__isModifyOp_x3f___spec__1___closed__3;
|
||||
lean_object* l_Lean_throwError___at_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop___main___spec__2(lean_object*);
|
||||
extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop___main___closed__3;
|
||||
lean_object* lean_instantiate_value_lparams(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_StructInst_throwFailedToElabField___rarg___closed__2;
|
||||
|
|
@ -849,7 +849,7 @@ lean_ctor_set(x_61, 0, x_60);
|
|||
lean_ctor_set(x_61, 1, x_59);
|
||||
x_62 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_63 = lean_array_push(x_62, x_61);
|
||||
x_64 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_64 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_65 = lean_array_push(x_63, x_64);
|
||||
x_66 = lean_array_push(x_65, x_40);
|
||||
x_67 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -894,7 +894,7 @@ lean_ctor_set(x_86, 0, x_85);
|
|||
lean_ctor_set(x_86, 1, x_84);
|
||||
x_87 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_88 = lean_array_push(x_87, x_86);
|
||||
x_89 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_89 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_90 = lean_array_push(x_88, x_89);
|
||||
x_91 = lean_array_push(x_90, x_40);
|
||||
x_92 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -1056,7 +1056,7 @@ lean_ctor_set(x_152, 0, x_151);
|
|||
lean_ctor_set(x_152, 1, x_150);
|
||||
x_153 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_154 = lean_array_push(x_153, x_152);
|
||||
x_155 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_155 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_156 = lean_array_push(x_154, x_155);
|
||||
x_157 = lean_array_push(x_156, x_130);
|
||||
x_158 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
@ -1290,7 +1290,7 @@ lean_ctor_set(x_231, 0, x_230);
|
|||
lean_ctor_set(x_231, 1, x_229);
|
||||
x_232 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__4;
|
||||
x_233 = lean_array_push(x_232, x_231);
|
||||
x_234 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__16;
|
||||
x_234 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__18;
|
||||
x_235 = lean_array_push(x_233, x_234);
|
||||
x_236 = lean_array_push(x_235, x_209);
|
||||
x_237 = l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___closed__2;
|
||||
|
|
|
|||
559
stage0/stdlib/Lean/Parser/Tactic.c
generated
559
stage0/stdlib/Lean/Parser/Tactic.c
generated
|
|
@ -125,6 +125,7 @@ extern lean_object* l_Lean_mkThunk___closed__1;
|
|||
lean_object* l_Lean_Parser_Tactic_admit___closed__5;
|
||||
lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_matchAlts_parenthesizer___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__7;
|
||||
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;
|
||||
|
|
@ -265,6 +266,7 @@ lean_object* l_Lean_Parser_Tactic_paren_parenthesizer___closed__2;
|
|||
lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_apply___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_orelse_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__6;
|
||||
lean_object* l_Lean_Parser_Tactic_done_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__6;
|
||||
|
|
@ -332,6 +334,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_focus___elambda__1___closed__5;
|
||||
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*);
|
||||
|
|
@ -342,6 +345,7 @@ lean_object* l_Lean_Parser_Tactic_induction_formatter___closed__5;
|
|||
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_matchAlts_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Tactic_focus_parenthesizer___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__18;
|
||||
lean_object* l_Lean_Parser_Tactic_withIds___closed__2;
|
||||
lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*);
|
||||
|
|
@ -439,6 +443,7 @@ lean_object* l_Lean_Parser_Tactic_case_formatter___closed__6;
|
|||
lean_object* l_Lean_Parser_Tactic_apply___closed__5;
|
||||
lean_object* l_Lean_Parser_Tactic_done_formatter___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_focus___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_changeWith_formatter___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_assumption___closed__4;
|
||||
|
|
@ -529,7 +534,9 @@ lean_object* l_Lean_Parser_Tactic_subst___closed__2;
|
|||
lean_object* l_Lean_Parser_Tactic_rewrite;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_injection_parenthesizer(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_refine_x21_formatter___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_focus___closed__4;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_let_formatter___closed__1;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_focus(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_generalizingVars___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_change___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_usingRec___elambda__1___closed__4;
|
||||
|
|
@ -537,6 +544,7 @@ lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__7;
|
|||
lean_object* l_Lean_Parser_Tactic_withIds_formatter___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_inductionAlts___elambda__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_failIfSuccess_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__6;
|
||||
lean_object* l_Lean_Parser_Tactic_traceState___closed__5;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_injection_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_changeWith_formatter___closed__5;
|
||||
|
|
@ -672,6 +680,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_failIfSuccess_formatter___closed_
|
|||
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Tactic_locationHyp___elambda__1___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__9;
|
||||
lean_object* l_Lean_Parser_Tactic_changeWith___closed__8;
|
||||
lean_object* l_Lean_Parser_Tactic_focus___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_change___closed__8;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_intros(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__6;
|
||||
|
|
@ -690,6 +699,7 @@ lean_object* l_Lean_Parser_Tactic_generalizingVars_formatter___closed__1;
|
|||
lean_object* l_Lean_Parser_Tactic_rewrite___closed__9;
|
||||
lean_object* l_Lean_Parser_Tactic_admit___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_matchAlts_parenthesizer___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_focus;
|
||||
lean_object* l_Lean_Parser_Tactic_rewrite_formatter___closed__7;
|
||||
lean_object* l_Lean_Parser_Tactic_intro_parenthesizer___closed__6;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_clear_formatter___closed__1;
|
||||
|
|
@ -705,6 +715,7 @@ lean_object* l_Lean_Parser_Tactic_let_x21___closed__2;
|
|||
lean_object* l_Lean_Parser_Tactic_changeWith_formatter___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_matchAlt___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_majorPremise_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_focus___closed__6;
|
||||
lean_object* l_Lean_Parser_Tactic_generalize_formatter___closed__10;
|
||||
lean_object* l_Lean_Parser_Tactic_changeWith___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_apply_formatter___closed__4;
|
||||
|
|
@ -790,6 +801,7 @@ lean_object* l_Lean_Parser_Tactic_let_formatter(lean_object*, lean_object*, lean
|
|||
lean_object* l_Lean_Parser_Tactic_ident_x27_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_generalize___closed__11;
|
||||
lean_object* l_Lean_Parser_Tactic_injection___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__2;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_match_formatter___closed__1;
|
||||
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_tupleTail___elambda__1___spec__1(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_rewrite___elambda__1___closed__3;
|
||||
|
|
@ -819,6 +831,7 @@ extern lean_object* l___regBuiltin_Lean_Parser_Term_syntheticHole_parenthesizer_
|
|||
lean_object* l_Lean_Parser_Tactic_admit___closed__2;
|
||||
lean_object* lean_name_mk_string(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_orelse_parenthesizer___closed__1;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_rwRuleSeq;
|
||||
lean_object* l_Lean_Parser_Tactic_rewrite___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_match___closed__2;
|
||||
|
|
@ -857,6 +870,7 @@ lean_object* l_Lean_Parser_Tactic_locationWildcard___elambda__1___closed__2;
|
|||
lean_object* l_Lean_Parser_Tactic_refine_formatter___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_traceState___closed__6;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_skip_parenthesizer(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_let___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_let_formatter___closed__1;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_clear_parenthesizer___closed__1;
|
||||
|
|
@ -898,6 +912,7 @@ lean_object* l_Lean_Parser_Tactic_induction_parenthesizer___closed__3;
|
|||
lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_let_x21___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_paren___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__8;
|
||||
lean_object* l_Lean_Parser_Tactic_inductionAlts_parenthesizer___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_majorPremise___closed__2;
|
||||
|
|
@ -937,6 +952,7 @@ lean_object* l_Lean_Parser_Tactic_introMatch___elambda__1___closed__3;
|
|||
lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_paren_formatter___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_focus___elambda__1___closed__4;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_admit_parenthesizer(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__7;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_failIfSuccess_parenthesizer___closed__1;
|
||||
|
|
@ -997,6 +1013,7 @@ lean_object* l_Lean_Parser_Tactic_rewriteSeq_parenthesizer___closed__3;
|
|||
lean_object* l_Lean_Parser_Tactic_subst___closed__3;
|
||||
lean_object* l_Lean_Parser_ParserState_popSyntax(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_usingRec_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_focus_formatter___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_paren_parenthesizer___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_subst_formatter___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_paren___elambda__1___closed__2;
|
||||
|
|
@ -1082,6 +1099,7 @@ lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__6;
|
|||
lean_object* l___regBuiltin_Lean_Parser_Tactic_refine_parenthesizer(lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_induction_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_location_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_focus_formatter___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__6;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_refine_formatter(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_intros___closed__9;
|
||||
|
|
@ -1131,6 +1149,7 @@ lean_object* l_Lean_Parser_Tactic_refine___closed__2;
|
|||
lean_object* l_Lean_Parser_Tactic_orelse_formatter___closed__1;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_exact(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_assumption___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_focus_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_show___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_location_formatter___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_majorPremise___closed__6;
|
||||
|
|
@ -1150,6 +1169,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_let_x21_formatter(lean_object*);
|
|||
lean_object* l_Lean_Parser_Tactic_locationTarget_parenthesizer___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_matchAlt_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_focus___closed__5;
|
||||
lean_object* l_Lean_Parser_Tactic_induction___elambda__1___closed__2;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_nestedTactic_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_generalize___elambda__1___closed__8;
|
||||
|
|
@ -1190,6 +1210,7 @@ lean_object* l_Lean_Parser_Tactic_cases___elambda__1___closed__3;
|
|||
lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__12;
|
||||
lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_have___elambda__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_focus_formatter___closed__3;
|
||||
extern lean_object* l_Lean_Parser_Term_let___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_revert___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_suffices;
|
||||
|
|
@ -1263,6 +1284,7 @@ lean_object* l_Lean_Parser_Tactic_rwRule_parenthesizer___closed__4;
|
|||
extern lean_object* l_Lean_Parser_epsilonInfo;
|
||||
lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_change___elambda__1___closed__3;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_assumption___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_done___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_locationWildcard___elambda__1(lean_object*, lean_object*);
|
||||
|
|
@ -1275,6 +1297,7 @@ extern lean_object* l_Lean_Parser_Term_typeAscription___closed__1;
|
|||
lean_object* l___regBuiltin_Lean_Parser_Tactic_changeWith_formatter(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_case_formatter___closed__5;
|
||||
lean_object* l_Lean_Parser_Tactic_majorPremise___elambda__1___closed__4;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_formatter(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_locationTarget___closed__5;
|
||||
lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_show_formatter___closed__1;
|
||||
|
|
@ -1301,6 +1324,7 @@ lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__6;
|
|||
lean_object* l_Lean_Parser_Tactic_suffices_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_traceState___elambda__1___closed__6;
|
||||
lean_object* l_Lean_Parser_Tactic_rwRule___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_focus_formatter___closed__4;
|
||||
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_inductionAlts___elambda__1___spec__1(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_change___elambda__1(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_match_parenthesizer___closed__3;
|
||||
|
|
@ -1355,6 +1379,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Tactic_paren(lean_object*);
|
|||
lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_matchAlt;
|
||||
lean_object* l_Lean_Parser_Tactic_done___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_focus___closed__7;
|
||||
lean_object* l_Lean_Parser_Tactic_locationHyp___elambda__1___closed__4;
|
||||
lean_object* l_String_trim(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_allGoals_formatter___closed__2;
|
||||
|
|
@ -1373,6 +1398,7 @@ lean_object* l_Lean_Parser_Tactic_matchAlt_formatter___closed__1;
|
|||
lean_object* l_Lean_Parser_Tactic_locationWildcard_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_change_parenthesizer___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_revert_parenthesizer___closed__3;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_rewrite_formatter___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_locationTarget;
|
||||
lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__5;
|
||||
|
|
@ -1428,6 +1454,7 @@ lean_object* l_Lean_Parser_Tactic_suffices___elambda__1___closed__3;
|
|||
lean_object* l_Lean_Parser_Tactic_rewrite_parenthesizer___closed__7;
|
||||
lean_object* l_Lean_Parser_Tactic_intro___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_exact_formatter___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_focus___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_generalize_formatter___closed__8;
|
||||
lean_object* l_Lean_Parser_Tactic_change___elambda__1___closed__8;
|
||||
lean_object* l_Lean_Parser_Term_syntheticHole___elambda__1(lean_object*, lean_object*);
|
||||
|
|
@ -1568,6 +1595,7 @@ lean_object* l_Lean_Parser_Tactic_assumption___elambda__1(lean_object*, lean_obj
|
|||
lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Tactic_matchAlts;
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_refine_x21_formatter(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_focus_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_locationTarget___elambda__1___closed__9;
|
||||
lean_object* l_Lean_Parser_Tactic_admit_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_refine_x21_formatter___closed__3;
|
||||
|
|
@ -1597,6 +1625,7 @@ lean_object* l_Lean_Parser_Tactic_subst___elambda__1___closed__4;
|
|||
lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__10;
|
||||
lean_object* l_Lean_Parser_Tactic_show_formatter___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_let_x21___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_focus_parenthesizer___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_locationHyp_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_matchAlts_formatter___closed__4;
|
||||
lean_object* l_Lean_PrettyPrinter_Formatter_notFollowedBy_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -1652,6 +1681,7 @@ lean_object* l_Lean_Parser_Tactic_rwRule___closed__5;
|
|||
lean_object* l___regBuiltin_Lean_Parser_Tactic_generalize_parenthesizer___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_underscore_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_skip___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_focus___elambda__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_rwRule___closed__7;
|
||||
lean_object* l_Lean_Parser_Tactic_rwRule_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_allGoals_formatter___closed__1;
|
||||
|
|
@ -9190,6 +9220,478 @@ 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_focus___elambda__1___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("focus");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___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_focus___elambda__1___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_Tactic_focus___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_focus___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_focus___elambda__1___closed__1;
|
||||
x_2 = l_Lean_Parser_Tactic_focus___elambda__1___closed__3;
|
||||
x_3 = 1;
|
||||
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("focus ");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__5;
|
||||
x_2 = l_String_trim(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__7() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Char_HasRepr___closed__1;
|
||||
x_2 = l_Lean_Parser_Tactic_focus___elambda__1___closed__6;
|
||||
x_3 = lean_string_append(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__8() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__7;
|
||||
x_2 = l_Char_HasRepr___closed__1;
|
||||
x_3 = lean_string_append(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_Tactic_focus___elambda__1(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
|
||||
x_3 = l_Lean_Parser_Tactic_tacticSeq;
|
||||
x_4 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_4);
|
||||
x_5 = l_Lean_Parser_Tactic_focus___elambda__1___closed__4;
|
||||
x_6 = lean_ctor_get(x_5, 1);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_2);
|
||||
lean_inc(x_1);
|
||||
x_7 = l_Lean_Parser_tryAnti(x_1, x_2);
|
||||
if (x_7 == 0)
|
||||
{
|
||||
lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
lean_dec(x_6);
|
||||
x_8 = lean_unsigned_to_nat(1024u);
|
||||
x_9 = l_Lean_Parser_checkPrecFn(x_8, x_1, x_2);
|
||||
x_10 = lean_ctor_get(x_9, 3);
|
||||
lean_inc(x_10);
|
||||
if (lean_obj_tag(x_10) == 0)
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
|
||||
x_11 = lean_ctor_get(x_9, 0);
|
||||
lean_inc(x_11);
|
||||
x_12 = lean_array_get_size(x_11);
|
||||
lean_dec(x_11);
|
||||
x_13 = l_Lean_Parser_Tactic_focus___elambda__1___closed__6;
|
||||
x_14 = l_Lean_Parser_Tactic_focus___elambda__1___closed__8;
|
||||
lean_inc(x_1);
|
||||
x_15 = l_Lean_Parser_nonReservedSymbolFnAux(x_13, x_14, x_1, x_9);
|
||||
x_16 = lean_ctor_get(x_15, 3);
|
||||
lean_inc(x_16);
|
||||
if (lean_obj_tag(x_16) == 0)
|
||||
{
|
||||
lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
x_17 = lean_apply_2(x_4, x_1, x_15);
|
||||
x_18 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2;
|
||||
x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_12);
|
||||
return x_19;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_20; lean_object* x_21;
|
||||
lean_dec(x_16);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_1);
|
||||
x_20 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2;
|
||||
x_21 = l_Lean_Parser_ParserState_mkNode(x_15, x_20, x_12);
|
||||
return x_21;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_1);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
|
||||
x_22 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_22);
|
||||
x_23 = lean_array_get_size(x_22);
|
||||
lean_dec(x_22);
|
||||
x_24 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_24);
|
||||
lean_inc(x_1);
|
||||
x_25 = lean_apply_2(x_6, x_1, x_2);
|
||||
x_26 = lean_ctor_get(x_25, 3);
|
||||
lean_inc(x_26);
|
||||
if (lean_obj_tag(x_26) == 0)
|
||||
{
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_23);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_1);
|
||||
return x_25;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_27; lean_object* x_28; uint8_t x_29;
|
||||
x_27 = lean_ctor_get(x_26, 0);
|
||||
lean_inc(x_27);
|
||||
lean_dec(x_26);
|
||||
x_28 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_28);
|
||||
x_29 = lean_nat_dec_eq(x_28, x_24);
|
||||
lean_dec(x_28);
|
||||
if (x_29 == 0)
|
||||
{
|
||||
lean_dec(x_27);
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_23);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_1);
|
||||
return x_25;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
|
||||
lean_inc(x_24);
|
||||
x_30 = l_Lean_Parser_ParserState_restore(x_25, x_23, x_24);
|
||||
lean_dec(x_23);
|
||||
x_31 = lean_unsigned_to_nat(1024u);
|
||||
x_32 = l_Lean_Parser_checkPrecFn(x_31, x_1, x_30);
|
||||
x_33 = lean_ctor_get(x_32, 3);
|
||||
lean_inc(x_33);
|
||||
if (lean_obj_tag(x_33) == 0)
|
||||
{
|
||||
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39;
|
||||
x_34 = lean_ctor_get(x_32, 0);
|
||||
lean_inc(x_34);
|
||||
x_35 = lean_array_get_size(x_34);
|
||||
lean_dec(x_34);
|
||||
x_36 = l_Lean_Parser_Tactic_focus___elambda__1___closed__6;
|
||||
x_37 = l_Lean_Parser_Tactic_focus___elambda__1___closed__8;
|
||||
lean_inc(x_1);
|
||||
x_38 = l_Lean_Parser_nonReservedSymbolFnAux(x_36, x_37, x_1, x_32);
|
||||
x_39 = lean_ctor_get(x_38, 3);
|
||||
lean_inc(x_39);
|
||||
if (lean_obj_tag(x_39) == 0)
|
||||
{
|
||||
lean_object* x_40; lean_object* x_41; lean_object* x_42; uint8_t x_43; lean_object* x_44;
|
||||
x_40 = lean_apply_2(x_4, x_1, x_38);
|
||||
x_41 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2;
|
||||
x_42 = l_Lean_Parser_ParserState_mkNode(x_40, x_41, x_35);
|
||||
x_43 = 1;
|
||||
x_44 = l_Lean_Parser_mergeOrElseErrors(x_42, x_27, x_24, x_43);
|
||||
lean_dec(x_24);
|
||||
return x_44;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_45; lean_object* x_46; uint8_t x_47; lean_object* x_48;
|
||||
lean_dec(x_39);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_1);
|
||||
x_45 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2;
|
||||
x_46 = l_Lean_Parser_ParserState_mkNode(x_38, x_45, x_35);
|
||||
x_47 = 1;
|
||||
x_48 = l_Lean_Parser_mergeOrElseErrors(x_46, x_27, x_24, x_47);
|
||||
lean_dec(x_24);
|
||||
return x_48;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_49; lean_object* x_50;
|
||||
lean_dec(x_33);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_1);
|
||||
x_49 = 1;
|
||||
x_50 = l_Lean_Parser_mergeOrElseErrors(x_32, x_27, x_24, x_49);
|
||||
lean_dec(x_24);
|
||||
return x_50;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__6;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Tactic_tacticSeq;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l_Lean_Parser_Tactic_focus___closed__1;
|
||||
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2;
|
||||
x_2 = l_Lean_Parser_Tactic_focus___closed__2;
|
||||
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___closed__4() {
|
||||
_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_focus___closed__3;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__4;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l_Lean_Parser_Tactic_focus___closed__4;
|
||||
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_focus___elambda__1), 2, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus___closed__7() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_focus___closed__5;
|
||||
x_2 = l_Lean_Parser_Tactic_focus___closed__6;
|
||||
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_focus() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Parser_Tactic_focus___closed__7;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_focus(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2;
|
||||
x_3 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2;
|
||||
x_4 = 1;
|
||||
x_5 = l_Lean_Parser_Tactic_focus;
|
||||
x_6 = lean_unsigned_to_nat(0u);
|
||||
x_7 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_6, x_1);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus_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_focus___elambda__1___closed__1;
|
||||
x_2 = l_Lean_Parser_Tactic_focus___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_focus_formatter___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__5;
|
||||
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_nonReservedSymbol_formatter___boxed), 6, 1);
|
||||
lean_closure_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus_formatter___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_focus_formatter___closed__2;
|
||||
x_2 = l_Lean_Parser_Term_byTactic_formatter___closed__3;
|
||||
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
|
||||
lean_closure_set(x_3, 0, x_1);
|
||||
lean_closure_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_focus_formatter___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_focus___elambda__1___closed__2;
|
||||
x_2 = lean_unsigned_to_nat(1024u);
|
||||
x_3 = l_Lean_Parser_Tactic_focus_formatter___closed__3;
|
||||
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
|
||||
lean_closure_set(x_4, 0, x_1);
|
||||
lean_closure_set(x_4, 1, x_2);
|
||||
lean_closure_set(x_4, 2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_Tactic_focus_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_Parser_Tactic_focus_formatter___closed__1;
|
||||
x_7 = l_Lean_Parser_Tactic_focus_formatter___closed__4;
|
||||
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_focus_formatter), 5, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_formatter(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_PrettyPrinter_formatterAttribute;
|
||||
x_3 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2;
|
||||
x_4 = l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1;
|
||||
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_focus_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_focus___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_focus_parenthesizer___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2;
|
||||
x_2 = lean_unsigned_to_nat(1024u);
|
||||
x_3 = l_Lean_Parser_Tactic_allGoals_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_focus_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_Parser_Tactic_focus_parenthesizer___closed__1;
|
||||
x_7 = l_Lean_Parser_Tactic_focus_parenthesizer___closed__2;
|
||||
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;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_focus_parenthesizer), 5, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer(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_PrettyPrinter_parenthesizerAttribute;
|
||||
x_3 = l_Lean_Parser_Tactic_focus___elambda__1___closed__2;
|
||||
x_4 = l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1;
|
||||
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_skip___elambda__1___closed__1() {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -31402,6 +31904,63 @@ lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_allGoals_parenthesizer___
|
|||
res = l___regBuiltin_Lean_Parser_Tactic_allGoals_parenthesizer(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Parser_Tactic_focus___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__1);
|
||||
l_Lean_Parser_Tactic_focus___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__2);
|
||||
l_Lean_Parser_Tactic_focus___elambda__1___closed__3 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__3();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__3);
|
||||
l_Lean_Parser_Tactic_focus___elambda__1___closed__4 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__4();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__4);
|
||||
l_Lean_Parser_Tactic_focus___elambda__1___closed__5 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__5();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__5);
|
||||
l_Lean_Parser_Tactic_focus___elambda__1___closed__6 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__6();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__6);
|
||||
l_Lean_Parser_Tactic_focus___elambda__1___closed__7 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__7();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__7);
|
||||
l_Lean_Parser_Tactic_focus___elambda__1___closed__8 = _init_l_Lean_Parser_Tactic_focus___elambda__1___closed__8();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___elambda__1___closed__8);
|
||||
l_Lean_Parser_Tactic_focus___closed__1 = _init_l_Lean_Parser_Tactic_focus___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__1);
|
||||
l_Lean_Parser_Tactic_focus___closed__2 = _init_l_Lean_Parser_Tactic_focus___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__2);
|
||||
l_Lean_Parser_Tactic_focus___closed__3 = _init_l_Lean_Parser_Tactic_focus___closed__3();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__3);
|
||||
l_Lean_Parser_Tactic_focus___closed__4 = _init_l_Lean_Parser_Tactic_focus___closed__4();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__4);
|
||||
l_Lean_Parser_Tactic_focus___closed__5 = _init_l_Lean_Parser_Tactic_focus___closed__5();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__5);
|
||||
l_Lean_Parser_Tactic_focus___closed__6 = _init_l_Lean_Parser_Tactic_focus___closed__6();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__6);
|
||||
l_Lean_Parser_Tactic_focus___closed__7 = _init_l_Lean_Parser_Tactic_focus___closed__7();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus___closed__7);
|
||||
l_Lean_Parser_Tactic_focus = _init_l_Lean_Parser_Tactic_focus();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus);
|
||||
res = l___regBuiltinParser_Lean_Parser_Tactic_focus(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Parser_Tactic_focus_formatter___closed__1 = _init_l_Lean_Parser_Tactic_focus_formatter___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus_formatter___closed__1);
|
||||
l_Lean_Parser_Tactic_focus_formatter___closed__2 = _init_l_Lean_Parser_Tactic_focus_formatter___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus_formatter___closed__2);
|
||||
l_Lean_Parser_Tactic_focus_formatter___closed__3 = _init_l_Lean_Parser_Tactic_focus_formatter___closed__3();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus_formatter___closed__3);
|
||||
l_Lean_Parser_Tactic_focus_formatter___closed__4 = _init_l_Lean_Parser_Tactic_focus_formatter___closed__4();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus_formatter___closed__4);
|
||||
l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_focus_formatter___closed__1);
|
||||
res = l___regBuiltin_Lean_Parser_Tactic_focus_formatter(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Parser_Tactic_focus_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_focus_parenthesizer___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus_parenthesizer___closed__1);
|
||||
l_Lean_Parser_Tactic_focus_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_focus_parenthesizer___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_focus_parenthesizer___closed__2);
|
||||
l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer___closed__1);
|
||||
res = l___regBuiltin_Lean_Parser_Tactic_focus_parenthesizer(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Parser_Tactic_skip___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_skip___elambda__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Tactic_skip___elambda__1___closed__1);
|
||||
l_Lean_Parser_Tactic_skip___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_skip___elambda__1___closed__2();
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue