chore: update stage0
This commit is contained in:
Lean stage0 autoupdater
parent
112fa51e08
commit
6d30aeefe5
8 changed files with 22337 additions and 6004 deletions
|
|
@ -1,7 +1,5 @@
|
|||
#include "util/options.h"
|
||||
|
||||
// CI, please update stage0
|
||||
|
||||
namespace lean {
|
||||
options get_default_options() {
|
||||
options opts;
|
||||
|
|
|
|||
1601
stage0/stdlib/Init/TacticsExtra.c
generated
1601
stage0/stdlib/Init/TacticsExtra.c
generated
File diff suppressed because it is too large
Load diff
7403
stage0/stdlib/Lean/Elab/BuiltinNotation.c
generated
7403
stage0/stdlib/Lean/Elab/BuiltinNotation.c
generated
File diff suppressed because it is too large
Load diff
14582
stage0/stdlib/Lean/Elab/DocString/Builtin.c
generated
14582
stage0/stdlib/Lean/Elab/DocString/Builtin.c
generated
File diff suppressed because it is too large
Load diff
4069
stage0/stdlib/Lean/Elab/DocString/Builtin/Keywords.c
generated
4069
stage0/stdlib/Lean/Elab/DocString/Builtin/Keywords.c
generated
File diff suppressed because it is too large
Load diff
114
stage0/stdlib/Lean/Elab/MutualDef.c
generated
114
stage0/stdlib/Lean/Elab/MutualDef.c
generated
|
|
@ -44325,15 +44325,41 @@ lean_inc_ref(x_6);
|
|||
x_22 = lean_apply_8(x_3, x_20, x_4, x_5, x_6, x_7, x_8, x_9, x_21);
|
||||
if (lean_obj_tag(x_22) == 0)
|
||||
{
|
||||
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
|
||||
lean_object* x_23; lean_object* x_24; uint8_t x_25;
|
||||
x_23 = lean_ctor_get(x_22, 0);
|
||||
lean_inc(x_23);
|
||||
x_24 = lean_ctor_get(x_22, 1);
|
||||
lean_inc(x_24);
|
||||
lean_dec_ref(x_22);
|
||||
x_25 = lean_box(0);
|
||||
x_26 = l_Lean_Meta_mkAuxTheorem(x_23, x_1, x_12, x_25, x_2, x_6, x_7, x_8, x_9, x_24);
|
||||
return x_26;
|
||||
if (x_2 == 0)
|
||||
{
|
||||
x_25 = x_2;
|
||||
goto block_28;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_29;
|
||||
x_29 = l_Lean_Expr_hasSorry(x_1);
|
||||
if (x_29 == 0)
|
||||
{
|
||||
x_25 = x_2;
|
||||
goto block_28;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_30;
|
||||
x_30 = 0;
|
||||
x_25 = x_30;
|
||||
goto block_28;
|
||||
}
|
||||
}
|
||||
block_28:
|
||||
{
|
||||
lean_object* x_26; lean_object* x_27;
|
||||
x_26 = lean_box(0);
|
||||
x_27 = l_Lean_Meta_mkAuxTheorem(x_23, x_1, x_12, x_26, x_25, x_6, x_7, x_8, x_9, x_24);
|
||||
return x_27;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -46893,7 +46919,7 @@ lean_inc_ref(x_8);
|
|||
x_14 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Elab_MutualDef_0__Lean_Elab_Term_fillHolesFromWhereFinally_spec__1(x_12, x_13, x_2, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
{
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_55; uint8_t x_56; lean_object* x_57; uint8_t x_58; uint8_t x_59; lean_object* x_60; lean_object* x_70; uint8_t x_71; lean_object* x_72; uint8_t x_73; lean_object* x_74; lean_object* x_86; lean_object* x_104; lean_object* x_105; lean_object* x_106; uint8_t x_107;
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; uint8_t x_20; uint8_t x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_55; lean_object* x_56; uint8_t x_57; lean_object* x_58; uint8_t x_59; lean_object* x_60; uint8_t x_70; lean_object* x_71; uint8_t x_72; lean_object* x_73; lean_object* x_74; lean_object* x_86; lean_object* x_104; lean_object* x_105; lean_object* x_106; uint8_t x_107;
|
||||
x_15 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_15);
|
||||
x_16 = lean_ctor_get(x_14, 1);
|
||||
|
|
@ -46943,20 +46969,20 @@ lean_inc(x_32);
|
|||
x_33 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_33);
|
||||
lean_dec_ref(x_3);
|
||||
x_34 = l_Array_isEmpty___redArg(x_20);
|
||||
lean_dec_ref(x_20);
|
||||
x_34 = l_Array_isEmpty___redArg(x_22);
|
||||
lean_dec_ref(x_22);
|
||||
x_35 = 1;
|
||||
x_36 = lean_box(x_34);
|
||||
x_37 = lean_box(x_19);
|
||||
x_38 = lean_box(x_35);
|
||||
x_39 = lean_box(x_22);
|
||||
x_39 = lean_box(x_21);
|
||||
x_40 = lean_box(x_11);
|
||||
x_41 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_fillHolesFromWhereFinally___boxed__const__1;
|
||||
x_42 = lean_alloc_closure((void*)(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_fillHolesFromWhereFinally___lam__3___boxed), 17, 10);
|
||||
lean_closure_set(x_42, 0, x_36);
|
||||
lean_closure_set(x_42, 1, x_37);
|
||||
lean_closure_set(x_42, 2, x_24);
|
||||
lean_closure_set(x_42, 3, x_21);
|
||||
lean_closure_set(x_42, 3, x_23);
|
||||
lean_closure_set(x_42, 4, x_38);
|
||||
lean_closure_set(x_42, 5, x_39);
|
||||
lean_closure_set(x_42, 6, x_40);
|
||||
|
|
@ -46995,7 +47021,7 @@ x_50 = lean_alloc_closure((void*)(l___private_Lean_Elab_MutualDef_0__Lean_Elab_T
|
|||
lean_closure_set(x_50, 0, x_43);
|
||||
lean_closure_set(x_50, 1, x_48);
|
||||
lean_closure_set(x_50, 2, x_49);
|
||||
if (x_23 == 0)
|
||||
if (x_20 == 0)
|
||||
{
|
||||
lean_object* x_51;
|
||||
x_51 = l_Lean_withExporting___at___Lean_withoutExporting___at___Lean_Meta_abstractProof___at_____private_Lean_Elab_MutualDef_0__Lean_Elab_Term_fillHolesFromWhereFinally_spec__9_spec__9_spec__9___redArg(x_50, x_11, x_25, x_26, x_27, x_28, x_29, x_30, x_31);
|
||||
|
|
@ -47006,7 +47032,7 @@ else
|
|||
if (x_19 == 0)
|
||||
{
|
||||
lean_object* x_52;
|
||||
x_52 = l_Lean_withExporting___at___Lean_withoutExporting___at___Lean_Meta_abstractProof___at_____private_Lean_Elab_MutualDef_0__Lean_Elab_Term_fillHolesFromWhereFinally_spec__9_spec__9_spec__9___redArg(x_50, x_23, x_25, x_26, x_27, x_28, x_29, x_30, x_31);
|
||||
x_52 = l_Lean_withExporting___at___Lean_withoutExporting___at___Lean_Meta_abstractProof___at_____private_Lean_Elab_MutualDef_0__Lean_Elab_Term_fillHolesFromWhereFinally_spec__9_spec__9_spec__9___redArg(x_50, x_20, x_25, x_26, x_27, x_28, x_29, x_30, x_31);
|
||||
return x_52;
|
||||
}
|
||||
else
|
||||
|
|
@ -47020,9 +47046,9 @@ return x_53;
|
|||
block_69:
|
||||
{
|
||||
size_t x_61; lean_object* x_62;
|
||||
x_61 = lean_array_size(x_57);
|
||||
lean_inc_ref(x_57);
|
||||
x_62 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Elab_MutualDef_0__Lean_Elab_Term_fillHolesFromWhereFinally_spec__19___redArg(x_61, x_13, x_57, x_6, x_7, x_8, x_9, x_60);
|
||||
x_61 = lean_array_size(x_58);
|
||||
lean_inc_ref(x_58);
|
||||
x_62 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Elab_MutualDef_0__Lean_Elab_Term_fillHolesFromWhereFinally_spec__19___redArg(x_61, x_13, x_58, x_6, x_7, x_8, x_9, x_60);
|
||||
if (lean_obj_tag(x_62) == 0)
|
||||
{
|
||||
lean_object* x_63; lean_object* x_64;
|
||||
|
|
@ -47034,8 +47060,8 @@ lean_dec_ref(x_62);
|
|||
x_19 = x_59;
|
||||
x_20 = x_57;
|
||||
x_21 = x_55;
|
||||
x_22 = x_56;
|
||||
x_23 = x_58;
|
||||
x_22 = x_58;
|
||||
x_23 = x_56;
|
||||
x_24 = x_63;
|
||||
x_25 = x_4;
|
||||
x_26 = x_5;
|
||||
|
|
@ -47049,8 +47075,8 @@ goto block_54;
|
|||
else
|
||||
{
|
||||
uint8_t x_65;
|
||||
lean_dec_ref(x_57);
|
||||
lean_dec_ref(x_55);
|
||||
lean_dec_ref(x_58);
|
||||
lean_dec_ref(x_56);
|
||||
lean_dec_ref(x_18);
|
||||
lean_dec(x_9);
|
||||
lean_dec_ref(x_8);
|
||||
|
|
@ -47096,13 +47122,13 @@ lean_inc(x_77);
|
|||
lean_dec_ref(x_74);
|
||||
x_78 = lean_unbox(x_75);
|
||||
lean_dec(x_75);
|
||||
lean_inc_ref(x_72);
|
||||
lean_inc_ref(x_73);
|
||||
x_19 = x_78;
|
||||
x_20 = x_72;
|
||||
x_21 = x_70;
|
||||
x_22 = x_71;
|
||||
x_23 = x_73;
|
||||
x_24 = x_72;
|
||||
x_22 = x_73;
|
||||
x_23 = x_71;
|
||||
x_24 = x_73;
|
||||
x_25 = x_4;
|
||||
x_26 = x_5;
|
||||
x_27 = x_6;
|
||||
|
|
@ -47132,8 +47158,8 @@ goto block_69;
|
|||
else
|
||||
{
|
||||
uint8_t x_81;
|
||||
lean_dec_ref(x_72);
|
||||
lean_dec_ref(x_70);
|
||||
lean_dec_ref(x_73);
|
||||
lean_dec_ref(x_71);
|
||||
lean_dec_ref(x_18);
|
||||
lean_dec(x_9);
|
||||
lean_dec_ref(x_8);
|
||||
|
|
@ -47182,10 +47208,10 @@ lean_inc(x_91);
|
|||
lean_dec_ref(x_87);
|
||||
lean_inc_ref_n(x_86, 2);
|
||||
x_19 = x_90;
|
||||
x_20 = x_86;
|
||||
x_21 = x_86;
|
||||
x_22 = x_90;
|
||||
x_23 = x_90;
|
||||
x_20 = x_90;
|
||||
x_21 = x_90;
|
||||
x_22 = x_86;
|
||||
x_23 = x_86;
|
||||
x_24 = x_86;
|
||||
x_25 = x_4;
|
||||
x_26 = x_5;
|
||||
|
|
@ -47211,10 +47237,10 @@ lean_object* x_96;
|
|||
lean_dec(x_94);
|
||||
x_96 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_fillHolesFromWhereFinally___lam__5(x_90, x_11, x_11, x_4, x_5, x_6, x_7, x_8, x_9, x_92);
|
||||
lean_inc_ref(x_86);
|
||||
x_70 = x_86;
|
||||
x_71 = x_90;
|
||||
x_72 = x_86;
|
||||
x_73 = x_90;
|
||||
x_70 = x_90;
|
||||
x_71 = x_86;
|
||||
x_72 = x_90;
|
||||
x_73 = x_86;
|
||||
x_74 = x_96;
|
||||
goto block_85;
|
||||
}
|
||||
|
|
@ -47224,10 +47250,10 @@ if (x_95 == 0)
|
|||
{
|
||||
lean_dec(x_94);
|
||||
lean_inc_ref(x_86);
|
||||
x_55 = x_86;
|
||||
x_56 = x_90;
|
||||
x_57 = x_86;
|
||||
x_58 = x_90;
|
||||
x_55 = x_90;
|
||||
x_56 = x_86;
|
||||
x_57 = x_90;
|
||||
x_58 = x_86;
|
||||
x_59 = x_90;
|
||||
x_60 = x_92;
|
||||
goto block_69;
|
||||
|
|
@ -47256,20 +47282,20 @@ x_101 = lean_unbox(x_99);
|
|||
lean_dec(x_99);
|
||||
x_102 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_fillHolesFromWhereFinally___lam__5(x_90, x_11, x_101, x_4, x_5, x_6, x_7, x_8, x_9, x_100);
|
||||
lean_inc_ref(x_86);
|
||||
x_70 = x_86;
|
||||
x_71 = x_90;
|
||||
x_72 = x_86;
|
||||
x_73 = x_90;
|
||||
x_70 = x_90;
|
||||
x_71 = x_86;
|
||||
x_72 = x_90;
|
||||
x_73 = x_86;
|
||||
x_74 = x_102;
|
||||
goto block_85;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc_ref(x_86);
|
||||
x_70 = x_86;
|
||||
x_71 = x_90;
|
||||
x_72 = x_86;
|
||||
x_73 = x_90;
|
||||
x_70 = x_90;
|
||||
x_71 = x_86;
|
||||
x_72 = x_90;
|
||||
x_73 = x_86;
|
||||
x_74 = x_98;
|
||||
goto block_85;
|
||||
}
|
||||
|
|
|
|||
437
stage0/stdlib/Lean/Elab/SyntheticMVars.c
generated
437
stage0/stdlib/Lean/Elab/SyntheticMVars.c
generated
|
|
@ -662,6 +662,7 @@ uint8_t l_Lean_instBEqInternalExceptionId_beq(lean_object*, lean_object*);
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizePendingInstMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___Lean_PersistentArray_forInAux___at___Lean_PersistentArray_forIn___at_____private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_throwStuckAtUniverseCnstr_spec__6_spec__6_spec__7_spec__7(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_DTreeMap_Internal_Impl_Const_get_x3f___at___Lean_instantiateLCtxMVars___at___Lean_instantiateMVarDeclMVars___at___Lean_Elab_Term_runTactic_spec__10_spec__10_spec__10___boxed(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Expr_hasSorry(lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___Lean_PersistentArray_forInAux___at___Lean_PersistentArray_forIn___at_____private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_throwStuckAtUniverseCnstr_spec__6_spec__6_spec__7(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Term_instReprPostponeBehavior_repr___closed__0;
|
||||
size_t lean_usize_sub(size_t, size_t);
|
||||
|
|
@ -21036,7 +21037,7 @@ return x_13;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_21; uint8_t x_32; lean_object* x_33; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; uint8_t x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_63; lean_object* x_74; lean_object* x_75; uint8_t x_76;
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_21; uint8_t x_32; lean_object* x_33; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; uint8_t x_42; lean_object* x_43; lean_object* x_44; uint8_t x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_63; lean_object* x_74; lean_object* x_75; uint8_t x_76;
|
||||
x_14 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_14);
|
||||
x_15 = lean_ctor_get(x_4, 1);
|
||||
|
|
@ -21319,15 +21320,15 @@ goto _start;
|
|||
block_47:
|
||||
{
|
||||
lean_object* x_45; lean_object* x_46;
|
||||
x_45 = l_Lean_addTrace___at_____private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeUsingDefaultPrio_synthesizeUsingDefaultInstance_spec__2___redArg(x_37, x_44, x_39, x_42, x_38, x_43, x_41);
|
||||
x_45 = l_Lean_addTrace___at_____private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeUsingDefaultPrio_synthesizeUsingDefaultInstance_spec__2___redArg(x_37, x_44, x_40, x_39, x_38, x_43, x_41);
|
||||
lean_dec(x_43);
|
||||
lean_dec_ref(x_38);
|
||||
lean_dec(x_42);
|
||||
lean_dec_ref(x_39);
|
||||
lean_dec(x_39);
|
||||
lean_dec_ref(x_40);
|
||||
x_46 = lean_ctor_get(x_45, 1);
|
||||
lean_inc(x_46);
|
||||
lean_dec_ref(x_45);
|
||||
x_32 = x_40;
|
||||
x_32 = x_42;
|
||||
x_33 = x_46;
|
||||
goto block_35;
|
||||
}
|
||||
|
|
@ -21365,10 +21366,10 @@ lean_inc(x_58);
|
|||
lean_dec_ref(x_54);
|
||||
x_59 = l_List_filterAuxM___at___List_filterAuxM___at_____private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep_spec__0_spec__0___closed__3;
|
||||
x_38 = x_51;
|
||||
x_39 = x_49;
|
||||
x_40 = x_48;
|
||||
x_39 = x_50;
|
||||
x_40 = x_49;
|
||||
x_41 = x_58;
|
||||
x_42 = x_50;
|
||||
x_42 = x_48;
|
||||
x_43 = x_52;
|
||||
x_44 = x_59;
|
||||
goto block_47;
|
||||
|
|
@ -21381,10 +21382,10 @@ lean_inc(x_60);
|
|||
lean_dec_ref(x_54);
|
||||
x_61 = l_List_filterAuxM___at___List_filterAuxM___at_____private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep_spec__0_spec__0___closed__6;
|
||||
x_38 = x_51;
|
||||
x_39 = x_49;
|
||||
x_40 = x_48;
|
||||
x_39 = x_50;
|
||||
x_40 = x_49;
|
||||
x_41 = x_60;
|
||||
x_42 = x_50;
|
||||
x_42 = x_48;
|
||||
x_43 = x_52;
|
||||
x_44 = x_61;
|
||||
goto block_47;
|
||||
|
|
@ -21763,10 +21764,10 @@ return x_34;
|
|||
block_47:
|
||||
{
|
||||
lean_object* x_45; lean_object* x_46;
|
||||
x_45 = l_Lean_addTrace___at_____private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeUsingDefaultPrio_synthesizeUsingDefaultInstance_spec__2___redArg(x_37, x_44, x_41, x_40, x_39, x_43, x_38);
|
||||
lean_dec(x_43);
|
||||
lean_dec_ref(x_39);
|
||||
x_45 = l_Lean_addTrace___at_____private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeUsingDefaultPrio_synthesizeUsingDefaultInstance_spec__2___redArg(x_37, x_44, x_41, x_43, x_39, x_40, x_38);
|
||||
lean_dec(x_40);
|
||||
lean_dec_ref(x_39);
|
||||
lean_dec(x_43);
|
||||
lean_dec_ref(x_41);
|
||||
x_46 = lean_ctor_get(x_45, 1);
|
||||
lean_inc(x_46);
|
||||
|
|
@ -21810,10 +21811,10 @@ lean_dec_ref(x_54);
|
|||
x_59 = l_List_filterAuxM___at___List_filterAuxM___at_____private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep_spec__0_spec__0___closed__3;
|
||||
x_38 = x_58;
|
||||
x_39 = x_51;
|
||||
x_40 = x_50;
|
||||
x_40 = x_52;
|
||||
x_41 = x_49;
|
||||
x_42 = x_48;
|
||||
x_43 = x_52;
|
||||
x_43 = x_50;
|
||||
x_44 = x_59;
|
||||
goto block_47;
|
||||
}
|
||||
|
|
@ -21826,10 +21827,10 @@ lean_dec_ref(x_54);
|
|||
x_61 = l_List_filterAuxM___at___List_filterAuxM___at_____private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep_spec__0_spec__0___closed__6;
|
||||
x_38 = x_60;
|
||||
x_39 = x_51;
|
||||
x_40 = x_50;
|
||||
x_40 = x_52;
|
||||
x_41 = x_49;
|
||||
x_42 = x_48;
|
||||
x_43 = x_52;
|
||||
x_43 = x_50;
|
||||
x_44 = x_61;
|
||||
goto block_47;
|
||||
}
|
||||
|
|
@ -24342,15 +24343,41 @@ lean_inc_ref(x_6);
|
|||
x_22 = lean_apply_8(x_3, x_20, x_4, x_5, x_6, x_7, x_8, x_9, x_21);
|
||||
if (lean_obj_tag(x_22) == 0)
|
||||
{
|
||||
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
|
||||
lean_object* x_23; lean_object* x_24; uint8_t x_25;
|
||||
x_23 = lean_ctor_get(x_22, 0);
|
||||
lean_inc(x_23);
|
||||
x_24 = lean_ctor_get(x_22, 1);
|
||||
lean_inc(x_24);
|
||||
lean_dec_ref(x_22);
|
||||
x_25 = lean_box(0);
|
||||
x_26 = l_Lean_Meta_mkAuxTheorem(x_23, x_1, x_12, x_25, x_2, x_6, x_7, x_8, x_9, x_24);
|
||||
return x_26;
|
||||
if (x_2 == 0)
|
||||
{
|
||||
x_25 = x_2;
|
||||
goto block_28;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_29;
|
||||
x_29 = l_Lean_Expr_hasSorry(x_1);
|
||||
if (x_29 == 0)
|
||||
{
|
||||
x_25 = x_2;
|
||||
goto block_28;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_30;
|
||||
x_30 = 0;
|
||||
x_25 = x_30;
|
||||
goto block_28;
|
||||
}
|
||||
}
|
||||
block_28:
|
||||
{
|
||||
lean_object* x_26; lean_object* x_27;
|
||||
x_26 = lean_box(0);
|
||||
x_27 = l_Lean_Meta_mkAuxTheorem(x_23, x_1, x_12, x_26, x_25, x_6, x_7, x_8, x_9, x_24);
|
||||
return x_27;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -24578,7 +24605,7 @@ return x_17;
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_Term_withNarrowedTacticReuse___at___Lean_Elab_Term_withNarrowedArgTacticReuse___at___Lean_Elab_Term_runTactic_spec__3_spec__3___redArg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_13; uint8_t x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; uint8_t x_18; uint8_t x_19; uint8_t x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27; uint8_t x_28; uint8_t x_29; lean_object* x_30; lean_object* x_31; uint8_t x_35; uint8_t x_36; lean_object* x_37; uint8_t x_38; lean_object* x_39; uint8_t x_40; uint8_t x_41; uint8_t x_42; lean_object* x_43; uint8_t x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; uint8_t x_48; uint8_t x_49; lean_object* x_50; lean_object* x_51; uint8_t x_52; uint8_t x_53; lean_object* x_54; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; uint8_t x_64; uint8_t x_65; uint8_t x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; uint8_t x_71; uint8_t x_72; uint8_t x_73; uint8_t x_74; uint8_t x_75; lean_object* x_76; uint8_t x_77; uint8_t x_78; uint8_t x_79; lean_object* x_80; lean_object* x_116;
|
||||
uint8_t x_13; lean_object* x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; uint8_t x_19; uint8_t x_20; lean_object* x_21; uint8_t x_22; uint8_t x_23; uint8_t x_24; uint8_t x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28; lean_object* x_29; uint8_t x_30; lean_object* x_31; uint8_t x_35; lean_object* x_36; uint8_t x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; uint8_t x_41; uint8_t x_42; uint8_t x_43; lean_object* x_44; uint8_t x_45; uint8_t x_46; uint8_t x_47; uint8_t x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; uint8_t x_52; uint8_t x_53; lean_object* x_54; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; uint8_t x_64; uint8_t x_65; uint8_t x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; uint8_t x_71; uint8_t x_72; uint8_t x_73; uint8_t x_74; uint8_t x_75; lean_object* x_76; uint8_t x_77; uint8_t x_78; uint8_t x_79; lean_object* x_80; lean_object* x_116;
|
||||
lean_inc_ref(x_1);
|
||||
x_58 = lean_apply_1(x_1, x_3);
|
||||
x_59 = lean_ctor_get(x_58, 0);
|
||||
|
|
@ -24645,25 +24672,25 @@ block_34:
|
|||
{
|
||||
lean_object* x_32; lean_object* x_33;
|
||||
x_32 = lean_alloc_ctor(0, 7, 11);
|
||||
lean_ctor_set(x_32, 0, x_21);
|
||||
lean_ctor_set(x_32, 0, x_17);
|
||||
lean_ctor_set(x_32, 1, x_26);
|
||||
lean_ctor_set(x_32, 2, x_25);
|
||||
lean_ctor_set(x_32, 3, x_15);
|
||||
lean_ctor_set(x_32, 4, x_17);
|
||||
lean_ctor_set(x_32, 5, x_30);
|
||||
lean_ctor_set(x_32, 2, x_21);
|
||||
lean_ctor_set(x_32, 3, x_29);
|
||||
lean_ctor_set(x_32, 4, x_14);
|
||||
lean_ctor_set(x_32, 5, x_16);
|
||||
lean_ctor_set(x_32, 6, x_31);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7, x_13);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 1, x_14);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 2, x_24);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 3, x_18);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 4, x_19);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 5, x_27);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 6, x_22);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 7, x_29);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 8, x_28);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 9, x_20);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 10, x_16);
|
||||
x_33 = lean_apply_9(x_23, x_4, x_5, x_32, x_7, x_8, x_9, x_10, x_11, x_12);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7, x_20);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 1, x_30);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 2, x_28);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 3, x_22);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 4, x_23);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 5, x_24);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 6, x_19);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 7, x_18);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 8, x_15);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 9, x_25);
|
||||
lean_ctor_set_uint8(x_32, sizeof(void*)*7 + 10, x_13);
|
||||
x_33 = lean_apply_9(x_27, x_4, x_5, x_32, x_7, x_8, x_9, x_10, x_11, x_12);
|
||||
return x_33;
|
||||
}
|
||||
block_57:
|
||||
|
|
@ -24671,27 +24698,27 @@ block_57:
|
|||
lean_object* x_55; lean_object* x_56;
|
||||
x_55 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_55, 0, x_54);
|
||||
lean_ctor_set(x_55, 1, x_47);
|
||||
lean_ctor_set(x_55, 1, x_39);
|
||||
x_56 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_56, 0, x_55);
|
||||
x_13 = x_35;
|
||||
x_14 = x_36;
|
||||
x_15 = x_37;
|
||||
x_16 = x_38;
|
||||
x_17 = x_39;
|
||||
x_18 = x_40;
|
||||
x_19 = x_41;
|
||||
x_20 = x_42;
|
||||
x_21 = x_43;
|
||||
x_22 = x_44;
|
||||
x_23 = x_45;
|
||||
x_24 = x_48;
|
||||
x_25 = x_46;
|
||||
x_26 = x_50;
|
||||
x_27 = x_49;
|
||||
x_28 = x_53;
|
||||
x_29 = x_52;
|
||||
x_30 = x_51;
|
||||
x_17 = x_40;
|
||||
x_18 = x_41;
|
||||
x_19 = x_42;
|
||||
x_20 = x_43;
|
||||
x_21 = x_44;
|
||||
x_22 = x_45;
|
||||
x_23 = x_46;
|
||||
x_24 = x_47;
|
||||
x_25 = x_48;
|
||||
x_26 = x_49;
|
||||
x_27 = x_50;
|
||||
x_28 = x_52;
|
||||
x_29 = x_51;
|
||||
x_30 = x_53;
|
||||
x_31 = x_56;
|
||||
goto block_34;
|
||||
}
|
||||
|
|
@ -24701,24 +24728,24 @@ if (lean_obj_tag(x_76) == 0)
|
|||
{
|
||||
lean_dec(x_59);
|
||||
lean_dec_ref(x_1);
|
||||
x_13 = x_64;
|
||||
x_14 = x_65;
|
||||
x_15 = x_68;
|
||||
x_16 = x_79;
|
||||
x_17 = x_69;
|
||||
x_18 = x_71;
|
||||
x_19 = x_72;
|
||||
x_20 = x_78;
|
||||
x_21 = x_62;
|
||||
x_22 = x_74;
|
||||
x_23 = x_80;
|
||||
x_24 = x_66;
|
||||
x_25 = x_67;
|
||||
x_13 = x_79;
|
||||
x_14 = x_69;
|
||||
x_15 = x_77;
|
||||
x_16 = x_70;
|
||||
x_17 = x_62;
|
||||
x_18 = x_75;
|
||||
x_19 = x_74;
|
||||
x_20 = x_64;
|
||||
x_21 = x_67;
|
||||
x_22 = x_71;
|
||||
x_23 = x_72;
|
||||
x_24 = x_73;
|
||||
x_25 = x_78;
|
||||
x_26 = x_63;
|
||||
x_27 = x_73;
|
||||
x_28 = x_77;
|
||||
x_29 = x_75;
|
||||
x_30 = x_70;
|
||||
x_27 = x_80;
|
||||
x_28 = x_66;
|
||||
x_29 = x_68;
|
||||
x_30 = x_65;
|
||||
x_31 = x_76;
|
||||
goto block_34;
|
||||
}
|
||||
|
|
@ -24738,25 +24765,25 @@ lean_dec_ref(x_1);
|
|||
x_83 = lean_ctor_get(x_81, 1);
|
||||
lean_inc(x_83);
|
||||
lean_dec(x_81);
|
||||
x_35 = x_64;
|
||||
x_36 = x_65;
|
||||
x_37 = x_68;
|
||||
x_38 = x_79;
|
||||
x_39 = x_69;
|
||||
x_40 = x_71;
|
||||
x_41 = x_72;
|
||||
x_42 = x_78;
|
||||
x_43 = x_62;
|
||||
x_44 = x_74;
|
||||
x_45 = x_80;
|
||||
x_46 = x_67;
|
||||
x_47 = x_83;
|
||||
x_48 = x_66;
|
||||
x_49 = x_73;
|
||||
x_50 = x_63;
|
||||
x_51 = x_70;
|
||||
x_52 = x_75;
|
||||
x_53 = x_77;
|
||||
x_35 = x_79;
|
||||
x_36 = x_69;
|
||||
x_37 = x_77;
|
||||
x_38 = x_70;
|
||||
x_39 = x_83;
|
||||
x_40 = x_62;
|
||||
x_41 = x_75;
|
||||
x_42 = x_74;
|
||||
x_43 = x_64;
|
||||
x_44 = x_67;
|
||||
x_45 = x_71;
|
||||
x_46 = x_72;
|
||||
x_47 = x_73;
|
||||
x_48 = x_78;
|
||||
x_49 = x_63;
|
||||
x_50 = x_80;
|
||||
x_51 = x_68;
|
||||
x_52 = x_66;
|
||||
x_53 = x_65;
|
||||
x_54 = x_82;
|
||||
goto block_57;
|
||||
}
|
||||
|
|
@ -24792,50 +24819,50 @@ lean_free_object(x_85);
|
|||
lean_dec(x_89);
|
||||
lean_free_object(x_82);
|
||||
x_94 = lean_box(0);
|
||||
x_35 = x_64;
|
||||
x_36 = x_65;
|
||||
x_37 = x_68;
|
||||
x_38 = x_79;
|
||||
x_39 = x_69;
|
||||
x_40 = x_71;
|
||||
x_41 = x_72;
|
||||
x_42 = x_78;
|
||||
x_43 = x_62;
|
||||
x_44 = x_74;
|
||||
x_45 = x_80;
|
||||
x_46 = x_67;
|
||||
x_47 = x_86;
|
||||
x_48 = x_66;
|
||||
x_49 = x_73;
|
||||
x_50 = x_63;
|
||||
x_51 = x_70;
|
||||
x_52 = x_75;
|
||||
x_53 = x_77;
|
||||
x_35 = x_79;
|
||||
x_36 = x_69;
|
||||
x_37 = x_77;
|
||||
x_38 = x_70;
|
||||
x_39 = x_86;
|
||||
x_40 = x_62;
|
||||
x_41 = x_75;
|
||||
x_42 = x_74;
|
||||
x_43 = x_64;
|
||||
x_44 = x_67;
|
||||
x_45 = x_71;
|
||||
x_46 = x_72;
|
||||
x_47 = x_73;
|
||||
x_48 = x_78;
|
||||
x_49 = x_63;
|
||||
x_50 = x_80;
|
||||
x_51 = x_68;
|
||||
x_52 = x_66;
|
||||
x_53 = x_65;
|
||||
x_54 = x_94;
|
||||
goto block_57;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_ctor_set(x_85, 0, x_92);
|
||||
x_35 = x_64;
|
||||
x_36 = x_65;
|
||||
x_37 = x_68;
|
||||
x_38 = x_79;
|
||||
x_39 = x_69;
|
||||
x_40 = x_71;
|
||||
x_41 = x_72;
|
||||
x_42 = x_78;
|
||||
x_43 = x_62;
|
||||
x_44 = x_74;
|
||||
x_45 = x_80;
|
||||
x_46 = x_67;
|
||||
x_47 = x_86;
|
||||
x_48 = x_66;
|
||||
x_49 = x_73;
|
||||
x_50 = x_63;
|
||||
x_51 = x_70;
|
||||
x_52 = x_75;
|
||||
x_53 = x_77;
|
||||
x_35 = x_79;
|
||||
x_36 = x_69;
|
||||
x_37 = x_77;
|
||||
x_38 = x_70;
|
||||
x_39 = x_86;
|
||||
x_40 = x_62;
|
||||
x_41 = x_75;
|
||||
x_42 = x_74;
|
||||
x_43 = x_64;
|
||||
x_44 = x_67;
|
||||
x_45 = x_71;
|
||||
x_46 = x_72;
|
||||
x_47 = x_73;
|
||||
x_48 = x_78;
|
||||
x_49 = x_63;
|
||||
x_50 = x_80;
|
||||
x_51 = x_68;
|
||||
x_52 = x_66;
|
||||
x_53 = x_65;
|
||||
x_54 = x_82;
|
||||
goto block_57;
|
||||
}
|
||||
|
|
@ -24862,25 +24889,25 @@ lean_dec(x_99);
|
|||
lean_dec(x_96);
|
||||
lean_free_object(x_82);
|
||||
x_101 = lean_box(0);
|
||||
x_35 = x_64;
|
||||
x_36 = x_65;
|
||||
x_37 = x_68;
|
||||
x_38 = x_79;
|
||||
x_39 = x_69;
|
||||
x_40 = x_71;
|
||||
x_41 = x_72;
|
||||
x_42 = x_78;
|
||||
x_43 = x_62;
|
||||
x_44 = x_74;
|
||||
x_45 = x_80;
|
||||
x_46 = x_67;
|
||||
x_47 = x_86;
|
||||
x_48 = x_66;
|
||||
x_49 = x_73;
|
||||
x_50 = x_63;
|
||||
x_51 = x_70;
|
||||
x_52 = x_75;
|
||||
x_53 = x_77;
|
||||
x_35 = x_79;
|
||||
x_36 = x_69;
|
||||
x_37 = x_77;
|
||||
x_38 = x_70;
|
||||
x_39 = x_86;
|
||||
x_40 = x_62;
|
||||
x_41 = x_75;
|
||||
x_42 = x_74;
|
||||
x_43 = x_64;
|
||||
x_44 = x_67;
|
||||
x_45 = x_71;
|
||||
x_46 = x_72;
|
||||
x_47 = x_73;
|
||||
x_48 = x_78;
|
||||
x_49 = x_63;
|
||||
x_50 = x_80;
|
||||
x_51 = x_68;
|
||||
x_52 = x_66;
|
||||
x_53 = x_65;
|
||||
x_54 = x_101;
|
||||
goto block_57;
|
||||
}
|
||||
|
|
@ -24891,25 +24918,25 @@ x_102 = lean_alloc_ctor(0, 2, 0);
|
|||
lean_ctor_set(x_102, 0, x_99);
|
||||
lean_ctor_set(x_102, 1, x_96);
|
||||
lean_ctor_set(x_82, 0, x_102);
|
||||
x_35 = x_64;
|
||||
x_36 = x_65;
|
||||
x_37 = x_68;
|
||||
x_38 = x_79;
|
||||
x_39 = x_69;
|
||||
x_40 = x_71;
|
||||
x_41 = x_72;
|
||||
x_42 = x_78;
|
||||
x_43 = x_62;
|
||||
x_44 = x_74;
|
||||
x_45 = x_80;
|
||||
x_46 = x_67;
|
||||
x_47 = x_86;
|
||||
x_48 = x_66;
|
||||
x_49 = x_73;
|
||||
x_50 = x_63;
|
||||
x_51 = x_70;
|
||||
x_52 = x_75;
|
||||
x_53 = x_77;
|
||||
x_35 = x_79;
|
||||
x_36 = x_69;
|
||||
x_37 = x_77;
|
||||
x_38 = x_70;
|
||||
x_39 = x_86;
|
||||
x_40 = x_62;
|
||||
x_41 = x_75;
|
||||
x_42 = x_74;
|
||||
x_43 = x_64;
|
||||
x_44 = x_67;
|
||||
x_45 = x_71;
|
||||
x_46 = x_72;
|
||||
x_47 = x_73;
|
||||
x_48 = x_78;
|
||||
x_49 = x_63;
|
||||
x_50 = x_80;
|
||||
x_51 = x_68;
|
||||
x_52 = x_66;
|
||||
x_53 = x_65;
|
||||
x_54 = x_82;
|
||||
goto block_57;
|
||||
}
|
||||
|
|
@ -24950,25 +24977,25 @@ lean_dec(x_110);
|
|||
lean_dec(x_107);
|
||||
lean_dec(x_106);
|
||||
x_112 = lean_box(0);
|
||||
x_35 = x_64;
|
||||
x_36 = x_65;
|
||||
x_37 = x_68;
|
||||
x_38 = x_79;
|
||||
x_39 = x_69;
|
||||
x_40 = x_71;
|
||||
x_41 = x_72;
|
||||
x_42 = x_78;
|
||||
x_43 = x_62;
|
||||
x_44 = x_74;
|
||||
x_45 = x_80;
|
||||
x_46 = x_67;
|
||||
x_47 = x_104;
|
||||
x_48 = x_66;
|
||||
x_49 = x_73;
|
||||
x_50 = x_63;
|
||||
x_51 = x_70;
|
||||
x_52 = x_75;
|
||||
x_53 = x_77;
|
||||
x_35 = x_79;
|
||||
x_36 = x_69;
|
||||
x_37 = x_77;
|
||||
x_38 = x_70;
|
||||
x_39 = x_104;
|
||||
x_40 = x_62;
|
||||
x_41 = x_75;
|
||||
x_42 = x_74;
|
||||
x_43 = x_64;
|
||||
x_44 = x_67;
|
||||
x_45 = x_71;
|
||||
x_46 = x_72;
|
||||
x_47 = x_73;
|
||||
x_48 = x_78;
|
||||
x_49 = x_63;
|
||||
x_50 = x_80;
|
||||
x_51 = x_68;
|
||||
x_52 = x_66;
|
||||
x_53 = x_65;
|
||||
x_54 = x_112;
|
||||
goto block_57;
|
||||
}
|
||||
|
|
@ -24984,25 +25011,25 @@ lean_ctor_set(x_113, 0, x_110);
|
|||
lean_ctor_set(x_113, 1, x_106);
|
||||
x_114 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_114, 0, x_113);
|
||||
x_35 = x_64;
|
||||
x_36 = x_65;
|
||||
x_37 = x_68;
|
||||
x_38 = x_79;
|
||||
x_39 = x_69;
|
||||
x_40 = x_71;
|
||||
x_41 = x_72;
|
||||
x_42 = x_78;
|
||||
x_43 = x_62;
|
||||
x_44 = x_74;
|
||||
x_45 = x_80;
|
||||
x_46 = x_67;
|
||||
x_47 = x_104;
|
||||
x_48 = x_66;
|
||||
x_49 = x_73;
|
||||
x_50 = x_63;
|
||||
x_51 = x_70;
|
||||
x_52 = x_75;
|
||||
x_53 = x_77;
|
||||
x_35 = x_79;
|
||||
x_36 = x_69;
|
||||
x_37 = x_77;
|
||||
x_38 = x_70;
|
||||
x_39 = x_104;
|
||||
x_40 = x_62;
|
||||
x_41 = x_75;
|
||||
x_42 = x_74;
|
||||
x_43 = x_64;
|
||||
x_44 = x_67;
|
||||
x_45 = x_71;
|
||||
x_46 = x_72;
|
||||
x_47 = x_73;
|
||||
x_48 = x_78;
|
||||
x_49 = x_63;
|
||||
x_50 = x_80;
|
||||
x_51 = x_68;
|
||||
x_52 = x_66;
|
||||
x_53 = x_65;
|
||||
x_54 = x_114;
|
||||
goto block_57;
|
||||
}
|
||||
|
|
|
|||
133
stage0/stdlib/Lean/Meta/AbstractNestedProofs.c
generated
133
stage0/stdlib/Lean/Meta/AbstractNestedProofs.c
generated
|
|
@ -119,7 +119,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentHashMap_0__Lean_Persist
|
|||
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___Lean_Meta_AbstractNestedProofs_visit_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_inferType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Meta_abstractNestedProofs___closed__4;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_abstractProof___redArg___lam__0(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_abstractProof___redArg___lam__0(lean_object*, uint8_t, lean_object*, uint8_t, lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_AssocList_replace___at___Std_DHashMap_Internal_Raw_u2080_insert___at___Lean_Meta_AbstractNestedProofs_visit_spec__1_spec__5___redArg(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_AssocList_replace___at___Std_DHashMap_Internal_Raw_u2080_insert___at___Lean_Meta_AbstractNestedProofs_visit_spec__1_spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -180,6 +180,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_lambdaLetTelescope___at___Lean_Meta_Abstrac
|
|||
lean_object* l_Nat_nextPowerOfTwo(lean_object*);
|
||||
lean_object* l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_AbstractNestedProofs_visit___lam__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Expr_hasSorry(lean_object*);
|
||||
size_t lean_usize_sub(size_t, size_t);
|
||||
static lean_object* l_Lean_withExporting___at___Lean_withoutExporting___at___Lean_Meta_abstractProof___at___Lean_Meta_AbstractNestedProofs_visit_spec__21_spec__21_spec__21___redArg___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_AbstractNestedProofs_visit___lam__4(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -219,21 +220,47 @@ lean_object* l_Lean_Meta_isProof(lean_object*, lean_object*, lean_object*, lean_
|
|||
size_t lean_usize_land(size_t, size_t);
|
||||
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___Lean_Meta_AbstractNestedProofs_visit_spec__14___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_withoutExporting___at___Lean_Meta_abstractProof___at___Lean_Meta_AbstractNestedProofs_visit_spec__21_spec__21(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_abstractProof___redArg___lam__0(lean_object* x_1, uint8_t x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_abstractProof___redArg___lam__0(lean_object* x_1, uint8_t x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_6 = lean_box(0);
|
||||
x_7 = lean_box(x_2);
|
||||
x_8 = lean_box(x_3);
|
||||
x_9 = lean_alloc_closure((void*)(l_Lean_Meta_mkAuxTheorem___boxed), 10, 5);
|
||||
lean_closure_set(x_9, 0, x_5);
|
||||
lean_closure_set(x_9, 1, x_1);
|
||||
lean_closure_set(x_9, 2, x_7);
|
||||
lean_closure_set(x_9, 3, x_6);
|
||||
lean_closure_set(x_9, 4, x_8);
|
||||
x_10 = lean_apply_2(x_4, lean_box(0), x_9);
|
||||
return x_10;
|
||||
uint8_t x_6;
|
||||
if (x_4 == 0)
|
||||
{
|
||||
x_6 = x_4;
|
||||
goto block_12;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_13;
|
||||
x_13 = l_Lean_Expr_hasSorry(x_1);
|
||||
if (x_13 == 0)
|
||||
{
|
||||
x_6 = x_4;
|
||||
goto block_12;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_14;
|
||||
x_14 = 0;
|
||||
x_6 = x_14;
|
||||
goto block_12;
|
||||
}
|
||||
}
|
||||
block_12:
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
x_7 = lean_box(0);
|
||||
x_8 = lean_box(x_2);
|
||||
x_9 = lean_box(x_6);
|
||||
x_10 = lean_alloc_closure((void*)(l_Lean_Meta_mkAuxTheorem___boxed), 10, 5);
|
||||
lean_closure_set(x_10, 0, x_5);
|
||||
lean_closure_set(x_10, 1, x_1);
|
||||
lean_closure_set(x_10, 2, x_8);
|
||||
lean_closure_set(x_10, 3, x_7);
|
||||
lean_closure_set(x_10, 4, x_9);
|
||||
x_11 = lean_apply_2(x_3, lean_box(0), x_10);
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_abstractProof___redArg___lam__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
|
|
@ -293,8 +320,8 @@ lean_inc(x_2);
|
|||
x_14 = lean_alloc_closure((void*)(l_Lean_Meta_abstractProof___redArg___lam__0___boxed), 5, 4);
|
||||
lean_closure_set(x_14, 0, x_5);
|
||||
lean_closure_set(x_14, 1, x_12);
|
||||
lean_closure_set(x_14, 2, x_13);
|
||||
lean_closure_set(x_14, 3, x_2);
|
||||
lean_closure_set(x_14, 2, x_2);
|
||||
lean_closure_set(x_14, 3, x_13);
|
||||
lean_inc(x_8);
|
||||
x_15 = lean_alloc_closure((void*)(l_Lean_Meta_abstractProof___redArg___lam__1), 4, 3);
|
||||
lean_closure_set(x_15, 0, x_7);
|
||||
|
|
@ -329,8 +356,8 @@ _start:
|
|||
{
|
||||
uint8_t x_6; uint8_t x_7; lean_object* x_8;
|
||||
x_6 = lean_unbox(x_2);
|
||||
x_7 = lean_unbox(x_3);
|
||||
x_8 = l_Lean_Meta_abstractProof___redArg___lam__0(x_1, x_6, x_7, x_4, x_5);
|
||||
x_7 = lean_unbox(x_4);
|
||||
x_8 = l_Lean_Meta_abstractProof___redArg___lam__0(x_1, x_6, x_3, x_7, x_5);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
|
|
@ -2116,11 +2143,11 @@ x_41 = lean_ctor_get(x_34, 1);
|
|||
lean_inc_ref(x_34);
|
||||
lean_inc(x_41);
|
||||
x_42 = l_Lean_PersistentHashMap_insert___at___Lean_Meta_AbstractNestedProofs_visit_spec__9___redArg(x_36, x_41, x_34);
|
||||
x_19 = x_42;
|
||||
x_19 = x_38;
|
||||
x_20 = x_35;
|
||||
x_21 = x_38;
|
||||
x_22 = x_34;
|
||||
x_23 = x_37;
|
||||
x_21 = x_42;
|
||||
x_22 = x_37;
|
||||
x_23 = x_34;
|
||||
x_24 = x_40;
|
||||
goto block_28;
|
||||
}
|
||||
|
|
@ -2140,13 +2167,13 @@ block_28:
|
|||
{
|
||||
lean_object* x_25; lean_object* x_26; lean_object* x_27;
|
||||
x_25 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_25, 0, x_22);
|
||||
x_26 = l_Lean_PersistentArray_set___redArg(x_23, x_24, x_25);
|
||||
lean_ctor_set(x_25, 0, x_23);
|
||||
x_26 = l_Lean_PersistentArray_set___redArg(x_22, x_24, x_25);
|
||||
lean_dec(x_24);
|
||||
x_27 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_27, 0, x_19);
|
||||
lean_ctor_set(x_27, 0, x_21);
|
||||
lean_ctor_set(x_27, 1, x_26);
|
||||
lean_ctor_set(x_27, 2, x_21);
|
||||
lean_ctor_set(x_27, 2, x_19);
|
||||
x_13 = x_27;
|
||||
x_14 = x_20;
|
||||
goto block_18;
|
||||
|
|
@ -2359,11 +2386,11 @@ x_41 = lean_ctor_get(x_34, 1);
|
|||
lean_inc_ref(x_34);
|
||||
lean_inc(x_41);
|
||||
x_42 = l_Lean_PersistentHashMap_insert___at___Lean_Meta_AbstractNestedProofs_visit_spec__9___redArg(x_36, x_41, x_34);
|
||||
x_19 = x_38;
|
||||
x_20 = x_34;
|
||||
x_21 = x_37;
|
||||
x_22 = x_35;
|
||||
x_23 = x_42;
|
||||
x_19 = x_42;
|
||||
x_20 = x_35;
|
||||
x_21 = x_38;
|
||||
x_22 = x_37;
|
||||
x_23 = x_34;
|
||||
x_24 = x_40;
|
||||
goto block_28;
|
||||
}
|
||||
|
|
@ -2381,15 +2408,15 @@ block_28:
|
|||
{
|
||||
lean_object* x_25; lean_object* x_26; lean_object* x_27;
|
||||
x_25 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_25, 0, x_20);
|
||||
x_26 = l_Lean_PersistentArray_set___redArg(x_21, x_24, x_25);
|
||||
lean_ctor_set(x_25, 0, x_23);
|
||||
x_26 = l_Lean_PersistentArray_set___redArg(x_22, x_24, x_25);
|
||||
lean_dec(x_24);
|
||||
x_27 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_27, 0, x_23);
|
||||
lean_ctor_set(x_27, 0, x_19);
|
||||
lean_ctor_set(x_27, 1, x_26);
|
||||
lean_ctor_set(x_27, 2, x_19);
|
||||
lean_ctor_set(x_27, 2, x_21);
|
||||
x_13 = x_27;
|
||||
x_14 = x_22;
|
||||
x_14 = x_20;
|
||||
goto block_18;
|
||||
}
|
||||
}
|
||||
|
|
@ -3473,15 +3500,41 @@ lean_inc_ref(x_6);
|
|||
x_23 = lean_apply_8(x_3, x_20, x_22, x_5, x_6, x_7, x_8, x_9, x_21);
|
||||
if (lean_obj_tag(x_23) == 0)
|
||||
{
|
||||
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
|
||||
lean_object* x_24; lean_object* x_25; uint8_t x_26;
|
||||
x_24 = lean_ctor_get(x_23, 0);
|
||||
lean_inc(x_24);
|
||||
x_25 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_25);
|
||||
lean_dec_ref(x_23);
|
||||
x_26 = lean_box(0);
|
||||
x_27 = l_Lean_Meta_mkAuxTheorem(x_24, x_1, x_12, x_26, x_2, x_6, x_7, x_8, x_9, x_25);
|
||||
return x_27;
|
||||
if (x_2 == 0)
|
||||
{
|
||||
x_26 = x_2;
|
||||
goto block_29;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_30;
|
||||
x_30 = l_Lean_Expr_hasSorry(x_1);
|
||||
if (x_30 == 0)
|
||||
{
|
||||
x_26 = x_2;
|
||||
goto block_29;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_31;
|
||||
x_31 = 0;
|
||||
x_26 = x_31;
|
||||
goto block_29;
|
||||
}
|
||||
}
|
||||
block_29:
|
||||
{
|
||||
lean_object* x_27; lean_object* x_28;
|
||||
x_27 = lean_box(0);
|
||||
x_28 = l_Lean_Meta_mkAuxTheorem(x_24, x_1, x_12, x_27, x_26, x_6, x_7, x_8, x_9, x_25);
|
||||
return x_28;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue