chore: update stage0
This commit is contained in:
Lean stage0 autoupdater
parent
e9a8b965aa
commit
50544489a9
31 changed files with 69489 additions and 68148 deletions
2
stage0/stdlib/Init/Data/String/Defs.c
generated
2
stage0/stdlib/Init/Data/String/Defs.c
generated
|
|
@ -885,7 +885,7 @@ _start:
|
|||
lean_object* v___x_281_; lean_object* v___x_282_; lean_object* v___x_283_; lean_object* v___x_284_; lean_object* v___x_285_; lean_object* v___x_286_;
|
||||
v___x_281_ = ((lean_object*)(l_String_Slice_getUTF8Byte_x21___closed__2));
|
||||
v___x_282_ = lean_unsigned_to_nat(4u);
|
||||
v___x_283_ = lean_unsigned_to_nat(509u);
|
||||
v___x_283_ = lean_unsigned_to_nat(512u);
|
||||
v___x_284_ = ((lean_object*)(l_String_Slice_getUTF8Byte_x21___closed__1));
|
||||
v___x_285_ = ((lean_object*)(l_String_Slice_getUTF8Byte_x21___closed__0));
|
||||
v___x_286_ = l_mkPanicMessageWithDecl(v___x_285_, v___x_284_, v___x_283_, v___x_282_, v___x_281_);
|
||||
|
|
|
|||
234
stage0/stdlib/Init/Data/String/Iter/Intercalate.c
generated
234
stage0/stdlib/Init/Data/String/Iter/Intercalate.c
generated
|
|
@ -20,13 +20,11 @@ LEAN_EXPORT lean_object* l_Std_Iter_joinString___redArg___lam__0(lean_object*, l
|
|||
static const lean_string_object l_Std_Iter_joinString___redArg___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 1, .m_capacity = 1, .m_length = 0, .m_data = ""};
|
||||
static const lean_object* l_Std_Iter_joinString___redArg___closed__0 = (const lean_object*)&l_Std_Iter_joinString___redArg___closed__0_value;
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_joinString___redArg(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_joinString(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_joinString___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_joinString(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___redArg___lam__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_joinString___redArg___lam__0(lean_object* v_inst_1_, lean_object* v_inst_2_, lean_object* v_it_3_, lean_object* v_acc_4_, lean_object* v_hP_5_, lean_object* v_recur_6_){
|
||||
_start:
|
||||
{
|
||||
|
|
@ -79,189 +77,171 @@ v___x_21_ = l_WellFounded_opaqueFix_u2083___redArg(v___f_19_, v_it_18_, v___x_20
|
|||
return v___x_21_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_joinString(lean_object* v_00_u03b1_22_, lean_object* v_00_u03b2_23_, lean_object* v_inst_24_, lean_object* v_inst_25_, lean_object* v_inst_26_, lean_object* v_it_27_){
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_joinString(lean_object* v_00_u03b1_22_, lean_object* v_00_u03b2_23_, lean_object* v_inst_24_, lean_object* v_inst_25_, lean_object* v_it_26_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_28_;
|
||||
v___x_28_ = l_Std_Iter_joinString___redArg(v_inst_24_, v_inst_26_, v_it_27_);
|
||||
return v___x_28_;
|
||||
lean_object* v___x_27_;
|
||||
v___x_27_ = l_Std_Iter_joinString___redArg(v_inst_24_, v_inst_25_, v_it_26_);
|
||||
return v___x_27_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_joinString___boxed(lean_object* v_00_u03b1_29_, lean_object* v_00_u03b2_30_, lean_object* v_inst_31_, lean_object* v_inst_32_, lean_object* v_inst_33_, lean_object* v_it_34_){
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___redArg___lam__0(lean_object* v_inst_28_, lean_object* v_inst_29_, lean_object* v_s_30_, lean_object* v_it_31_, lean_object* v_acc_32_, lean_object* v_hP_33_, lean_object* v_recur_34_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_35_;
|
||||
v_res_35_ = l_Std_Iter_joinString(v_00_u03b1_29_, v_00_u03b2_30_, v_inst_31_, v_inst_32_, v_inst_33_, v_it_34_);
|
||||
lean_dec(v_inst_32_);
|
||||
return v_res_35_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___redArg___lam__0(lean_object* v_inst_36_, lean_object* v_inst_37_, lean_object* v_s_38_, lean_object* v_it_39_, lean_object* v_acc_40_, lean_object* v_hP_41_, lean_object* v_recur_42_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_val_43_;
|
||||
v_val_43_ = lean_apply_1(v_inst_36_, v_it_39_);
|
||||
switch(lean_obj_tag(v_val_43_))
|
||||
lean_object* v_val_35_;
|
||||
v_val_35_ = lean_apply_1(v_inst_28_, v_it_31_);
|
||||
switch(lean_obj_tag(v_val_35_))
|
||||
{
|
||||
case 0:
|
||||
{
|
||||
lean_object* v_it_44_; lean_object* v_out_45_; lean_object* v___x_46_;
|
||||
v_it_44_ = lean_ctor_get(v_val_43_, 0);
|
||||
lean_inc(v_it_44_);
|
||||
v_out_45_ = lean_ctor_get(v_val_43_, 1);
|
||||
lean_inc(v_out_45_);
|
||||
lean_dec_ref(v_val_43_);
|
||||
v___x_46_ = lean_apply_1(v_inst_37_, v_out_45_);
|
||||
if (lean_obj_tag(v_acc_40_) == 0)
|
||||
lean_object* v_it_36_; lean_object* v_out_37_; lean_object* v___x_38_;
|
||||
v_it_36_ = lean_ctor_get(v_val_35_, 0);
|
||||
lean_inc(v_it_36_);
|
||||
v_out_37_ = lean_ctor_get(v_val_35_, 1);
|
||||
lean_inc(v_out_37_);
|
||||
lean_dec_ref(v_val_35_);
|
||||
v___x_38_ = lean_apply_1(v_inst_29_, v_out_37_);
|
||||
if (lean_obj_tag(v_acc_32_) == 0)
|
||||
{
|
||||
lean_object* v___x_47_; lean_object* v___x_48_;
|
||||
v___x_47_ = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(v___x_47_, 0, v___x_46_);
|
||||
v___x_48_ = lean_apply_4(v_recur_42_, v_it_44_, v___x_47_, lean_box(0), lean_box(0));
|
||||
return v___x_48_;
|
||||
lean_object* v___x_39_; lean_object* v___x_40_;
|
||||
v___x_39_ = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(v___x_39_, 0, v___x_38_);
|
||||
v___x_40_ = lean_apply_4(v_recur_34_, v_it_36_, v___x_39_, lean_box(0), lean_box(0));
|
||||
return v___x_40_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_val_49_; lean_object* v___x_51_; uint8_t v_isShared_52_; uint8_t v_isSharedCheck_63_;
|
||||
v_val_49_ = lean_ctor_get(v_acc_40_, 0);
|
||||
v_isSharedCheck_63_ = !lean_is_exclusive(v_acc_40_);
|
||||
if (v_isSharedCheck_63_ == 0)
|
||||
lean_object* v_val_41_; lean_object* v___x_43_; uint8_t v_isShared_44_; uint8_t v_isSharedCheck_55_;
|
||||
v_val_41_ = lean_ctor_get(v_acc_32_, 0);
|
||||
v_isSharedCheck_55_ = !lean_is_exclusive(v_acc_32_);
|
||||
if (v_isSharedCheck_55_ == 0)
|
||||
{
|
||||
v___x_51_ = v_acc_40_;
|
||||
v_isShared_52_ = v_isSharedCheck_63_;
|
||||
goto v_resetjp_50_;
|
||||
v___x_43_ = v_acc_32_;
|
||||
v_isShared_44_ = v_isSharedCheck_55_;
|
||||
goto v_resetjp_42_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_val_49_);
|
||||
lean_dec(v_acc_40_);
|
||||
v___x_51_ = lean_box(0);
|
||||
v_isShared_52_ = v_isSharedCheck_63_;
|
||||
goto v_resetjp_50_;
|
||||
lean_inc(v_val_41_);
|
||||
lean_dec(v_acc_32_);
|
||||
v___x_43_ = lean_box(0);
|
||||
v_isShared_44_ = v_isSharedCheck_55_;
|
||||
goto v_resetjp_42_;
|
||||
}
|
||||
v_resetjp_50_:
|
||||
v_resetjp_42_:
|
||||
{
|
||||
lean_object* v_str_53_; lean_object* v_startInclusive_54_; lean_object* v_endExclusive_55_; lean_object* v___x_56_; lean_object* v___x_57_; lean_object* v___x_58_; lean_object* v___x_60_;
|
||||
v_str_53_ = lean_ctor_get(v_s_38_, 0);
|
||||
v_startInclusive_54_ = lean_ctor_get(v_s_38_, 1);
|
||||
v_endExclusive_55_ = lean_ctor_get(v_s_38_, 2);
|
||||
v___x_56_ = lean_string_utf8_extract(v_str_53_, v_startInclusive_54_, v_endExclusive_55_);
|
||||
v___x_57_ = lean_string_append(v_val_49_, v___x_56_);
|
||||
lean_dec_ref(v___x_56_);
|
||||
v___x_58_ = lean_string_append(v___x_57_, v___x_46_);
|
||||
lean_dec_ref(v___x_46_);
|
||||
if (v_isShared_52_ == 0)
|
||||
lean_object* v_str_45_; lean_object* v_startInclusive_46_; lean_object* v_endExclusive_47_; lean_object* v___x_48_; lean_object* v___x_49_; lean_object* v___x_50_; lean_object* v___x_52_;
|
||||
v_str_45_ = lean_ctor_get(v_s_30_, 0);
|
||||
v_startInclusive_46_ = lean_ctor_get(v_s_30_, 1);
|
||||
v_endExclusive_47_ = lean_ctor_get(v_s_30_, 2);
|
||||
v___x_48_ = lean_string_utf8_extract(v_str_45_, v_startInclusive_46_, v_endExclusive_47_);
|
||||
v___x_49_ = lean_string_append(v_val_41_, v___x_48_);
|
||||
lean_dec_ref(v___x_48_);
|
||||
v___x_50_ = lean_string_append(v___x_49_, v___x_38_);
|
||||
lean_dec_ref(v___x_38_);
|
||||
if (v_isShared_44_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_51_, 0, v___x_58_);
|
||||
v___x_60_ = v___x_51_;
|
||||
goto v_reusejp_59_;
|
||||
lean_ctor_set(v___x_43_, 0, v___x_50_);
|
||||
v___x_52_ = v___x_43_;
|
||||
goto v_reusejp_51_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_62_;
|
||||
v_reuseFailAlloc_62_ = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(v_reuseFailAlloc_62_, 0, v___x_58_);
|
||||
v___x_60_ = v_reuseFailAlloc_62_;
|
||||
goto v_reusejp_59_;
|
||||
lean_object* v_reuseFailAlloc_54_;
|
||||
v_reuseFailAlloc_54_ = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(v_reuseFailAlloc_54_, 0, v___x_50_);
|
||||
v___x_52_ = v_reuseFailAlloc_54_;
|
||||
goto v_reusejp_51_;
|
||||
}
|
||||
v_reusejp_59_:
|
||||
v_reusejp_51_:
|
||||
{
|
||||
lean_object* v___x_61_;
|
||||
v___x_61_ = lean_apply_4(v_recur_42_, v_it_44_, v___x_60_, lean_box(0), lean_box(0));
|
||||
return v___x_61_;
|
||||
lean_object* v___x_53_;
|
||||
v___x_53_ = lean_apply_4(v_recur_34_, v_it_36_, v___x_52_, lean_box(0), lean_box(0));
|
||||
return v___x_53_;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
case 1:
|
||||
{
|
||||
lean_object* v_it_64_; lean_object* v___x_65_;
|
||||
lean_dec_ref(v_inst_37_);
|
||||
v_it_64_ = lean_ctor_get(v_val_43_, 0);
|
||||
lean_inc(v_it_64_);
|
||||
lean_dec_ref(v_val_43_);
|
||||
v___x_65_ = lean_apply_4(v_recur_42_, v_it_64_, v_acc_40_, lean_box(0), lean_box(0));
|
||||
return v___x_65_;
|
||||
lean_object* v_it_56_; lean_object* v___x_57_;
|
||||
lean_dec_ref(v_inst_29_);
|
||||
v_it_56_ = lean_ctor_get(v_val_35_, 0);
|
||||
lean_inc(v_it_56_);
|
||||
lean_dec_ref(v_val_35_);
|
||||
v___x_57_ = lean_apply_4(v_recur_34_, v_it_56_, v_acc_32_, lean_box(0), lean_box(0));
|
||||
return v___x_57_;
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_dec_ref(v_recur_42_);
|
||||
lean_dec_ref(v_inst_37_);
|
||||
return v_acc_40_;
|
||||
lean_dec_ref(v_recur_34_);
|
||||
lean_dec_ref(v_inst_29_);
|
||||
return v_acc_32_;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___redArg___lam__0___boxed(lean_object* v_inst_66_, lean_object* v_inst_67_, lean_object* v_s_68_, lean_object* v_it_69_, lean_object* v_acc_70_, lean_object* v_hP_71_, lean_object* v_recur_72_){
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___redArg___lam__0___boxed(lean_object* v_inst_58_, lean_object* v_inst_59_, lean_object* v_s_60_, lean_object* v_it_61_, lean_object* v_acc_62_, lean_object* v_hP_63_, lean_object* v_recur_64_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_73_;
|
||||
v_res_73_ = l_Std_Iter_intercalateString___redArg___lam__0(v_inst_66_, v_inst_67_, v_s_68_, v_it_69_, v_acc_70_, v_hP_71_, v_recur_72_);
|
||||
lean_dec_ref(v_s_68_);
|
||||
return v_res_73_;
|
||||
lean_object* v_res_65_;
|
||||
v_res_65_ = l_Std_Iter_intercalateString___redArg___lam__0(v_inst_58_, v_inst_59_, v_s_60_, v_it_61_, v_acc_62_, v_hP_63_, v_recur_64_);
|
||||
lean_dec_ref(v_s_60_);
|
||||
return v_res_65_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___redArg(lean_object* v_inst_74_, lean_object* v_inst_75_, lean_object* v_s_76_, lean_object* v_it_77_){
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___redArg(lean_object* v_inst_66_, lean_object* v_inst_67_, lean_object* v_s_68_, lean_object* v_it_69_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___f_78_; lean_object* v___x_79_; lean_object* v___x_80_;
|
||||
v___f_78_ = lean_alloc_closure((void*)(l_Std_Iter_intercalateString___redArg___lam__0___boxed), 7, 3);
|
||||
lean_closure_set(v___f_78_, 0, v_inst_74_);
|
||||
lean_closure_set(v___f_78_, 1, v_inst_75_);
|
||||
lean_closure_set(v___f_78_, 2, v_s_76_);
|
||||
v___x_79_ = lean_box(0);
|
||||
v___x_80_ = l_WellFounded_opaqueFix_u2083___redArg(v___f_78_, v_it_77_, v___x_79_, lean_box(0));
|
||||
if (lean_obj_tag(v___x_80_) == 0)
|
||||
lean_object* v___f_70_; lean_object* v___x_71_; lean_object* v___x_72_;
|
||||
v___f_70_ = lean_alloc_closure((void*)(l_Std_Iter_intercalateString___redArg___lam__0___boxed), 7, 3);
|
||||
lean_closure_set(v___f_70_, 0, v_inst_66_);
|
||||
lean_closure_set(v___f_70_, 1, v_inst_67_);
|
||||
lean_closure_set(v___f_70_, 2, v_s_68_);
|
||||
v___x_71_ = lean_box(0);
|
||||
v___x_72_ = l_WellFounded_opaqueFix_u2083___redArg(v___f_70_, v_it_69_, v___x_71_, lean_box(0));
|
||||
if (lean_obj_tag(v___x_72_) == 0)
|
||||
{
|
||||
lean_object* v___x_81_;
|
||||
v___x_81_ = ((lean_object*)(l_Std_Iter_joinString___redArg___closed__0));
|
||||
return v___x_81_;
|
||||
lean_object* v___x_73_;
|
||||
v___x_73_ = ((lean_object*)(l_Std_Iter_joinString___redArg___closed__0));
|
||||
return v___x_73_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_val_82_;
|
||||
v_val_82_ = lean_ctor_get(v___x_80_, 0);
|
||||
lean_inc(v_val_82_);
|
||||
lean_dec_ref(v___x_80_);
|
||||
return v_val_82_;
|
||||
lean_object* v_val_74_;
|
||||
v_val_74_ = lean_ctor_get(v___x_72_, 0);
|
||||
lean_inc(v_val_74_);
|
||||
lean_dec_ref(v___x_72_);
|
||||
return v_val_74_;
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString(lean_object* v_00_u03b1_83_, lean_object* v_00_u03b2_84_, lean_object* v_inst_85_, lean_object* v_inst_86_, lean_object* v_inst_87_, lean_object* v_s_88_, lean_object* v_it_89_){
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString(lean_object* v_00_u03b1_75_, lean_object* v_00_u03b2_76_, lean_object* v_inst_77_, lean_object* v_inst_78_, lean_object* v_s_79_, lean_object* v_it_80_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___f_90_; lean_object* v___x_91_; lean_object* v___x_92_;
|
||||
v___f_90_ = lean_alloc_closure((void*)(l_Std_Iter_intercalateString___redArg___lam__0___boxed), 7, 3);
|
||||
lean_closure_set(v___f_90_, 0, v_inst_85_);
|
||||
lean_closure_set(v___f_90_, 1, v_inst_87_);
|
||||
lean_closure_set(v___f_90_, 2, v_s_88_);
|
||||
v___x_91_ = lean_box(0);
|
||||
v___x_92_ = l_WellFounded_opaqueFix_u2083___redArg(v___f_90_, v_it_89_, v___x_91_, lean_box(0));
|
||||
if (lean_obj_tag(v___x_92_) == 0)
|
||||
lean_object* v___f_81_; lean_object* v___x_82_; lean_object* v___x_83_;
|
||||
v___f_81_ = lean_alloc_closure((void*)(l_Std_Iter_intercalateString___redArg___lam__0___boxed), 7, 3);
|
||||
lean_closure_set(v___f_81_, 0, v_inst_77_);
|
||||
lean_closure_set(v___f_81_, 1, v_inst_78_);
|
||||
lean_closure_set(v___f_81_, 2, v_s_79_);
|
||||
v___x_82_ = lean_box(0);
|
||||
v___x_83_ = l_WellFounded_opaqueFix_u2083___redArg(v___f_81_, v_it_80_, v___x_82_, lean_box(0));
|
||||
if (lean_obj_tag(v___x_83_) == 0)
|
||||
{
|
||||
lean_object* v___x_93_;
|
||||
v___x_93_ = ((lean_object*)(l_Std_Iter_joinString___redArg___closed__0));
|
||||
return v___x_93_;
|
||||
lean_object* v___x_84_;
|
||||
v___x_84_ = ((lean_object*)(l_Std_Iter_joinString___redArg___closed__0));
|
||||
return v___x_84_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_val_94_;
|
||||
v_val_94_ = lean_ctor_get(v___x_92_, 0);
|
||||
lean_inc(v_val_94_);
|
||||
lean_dec_ref(v___x_92_);
|
||||
return v_val_94_;
|
||||
lean_object* v_val_85_;
|
||||
v_val_85_ = lean_ctor_get(v___x_83_, 0);
|
||||
lean_inc(v_val_85_);
|
||||
lean_dec_ref(v___x_83_);
|
||||
return v_val_85_;
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Std_Iter_intercalateString___boxed(lean_object* v_00_u03b1_95_, lean_object* v_00_u03b2_96_, lean_object* v_inst_97_, lean_object* v_inst_98_, lean_object* v_inst_99_, lean_object* v_s_100_, lean_object* v_it_101_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_102_;
|
||||
v_res_102_ = l_Std_Iter_intercalateString(v_00_u03b1_95_, v_00_u03b2_96_, v_inst_97_, v_inst_98_, v_inst_99_, v_s_100_, v_it_101_);
|
||||
lean_dec(v_inst_98_);
|
||||
return v_res_102_;
|
||||
}
|
||||
}
|
||||
lean_object* runtime_initialize_Init_Data_Iterators_Combinators_Monadic_FilterMap(uint8_t builtin);
|
||||
lean_object* runtime_initialize_Init_Data_String_Basic(uint8_t builtin);
|
||||
lean_object* runtime_initialize_Init_Data_String_Slice(uint8_t builtin);
|
||||
|
|
|
|||
109
stage0/stdlib/Init/Data/String/Slice.c
generated
109
stage0/stdlib/Init/Data/String/Slice.c
generated
|
|
@ -406,6 +406,10 @@ LEAN_EXPORT lean_object* l___private_Init_Data_String_Slice_0__String_Slice_inte
|
|||
LEAN_EXPORT lean_object* l___private_Init_Data_String_Slice_0__String_Slice_intercalate_go___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_String_Slice_intercalate(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_String_Slice_intercalate___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_foldl___at___00String_Slice_join_spec__0(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_foldl___at___00String_Slice_join_spec__0___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_String_Slice_join(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_String_Slice_join___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_String_Slice_toName(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_String_Slice_toName___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_String_Slice_instToFormat___lam__0(lean_object*);
|
||||
|
|
@ -9628,46 +9632,97 @@ lean_dec_ref(v_s_3347_);
|
|||
return v_res_3349_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_String_Slice_toName(lean_object* v_s_3350_){
|
||||
LEAN_EXPORT lean_object* l_List_foldl___at___00String_Slice_join_spec__0(lean_object* v_x_3350_, lean_object* v_x_3351_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_3351_; lean_object* v___x_3352_;
|
||||
v___x_3351_ = l_String_Slice_toString(v_s_3350_);
|
||||
v___x_3352_ = l_String_toName(v___x_3351_);
|
||||
return v___x_3352_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_String_Slice_toName___boxed(lean_object* v_s_3353_){
|
||||
_start:
|
||||
if (lean_obj_tag(v_x_3351_) == 0)
|
||||
{
|
||||
lean_object* v_res_3354_;
|
||||
v_res_3354_ = l_String_Slice_toName(v_s_3353_);
|
||||
lean_dec_ref(v_s_3353_);
|
||||
return v_res_3354_;
|
||||
return v_x_3350_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_String_Slice_instToFormat___lam__0(lean_object* v_s_3355_){
|
||||
_start:
|
||||
else
|
||||
{
|
||||
lean_object* v_str_3356_; lean_object* v_startInclusive_3357_; lean_object* v_endExclusive_3358_; lean_object* v___x_3359_; lean_object* v___x_3360_;
|
||||
v_str_3356_ = lean_ctor_get(v_s_3355_, 0);
|
||||
v_startInclusive_3357_ = lean_ctor_get(v_s_3355_, 1);
|
||||
v_endExclusive_3358_ = lean_ctor_get(v_s_3355_, 2);
|
||||
v___x_3359_ = lean_string_utf8_extract(v_str_3356_, v_startInclusive_3357_, v_endExclusive_3358_);
|
||||
v___x_3360_ = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(v___x_3360_, 0, v___x_3359_);
|
||||
return v___x_3360_;
|
||||
lean_object* v_head_3352_; lean_object* v_tail_3353_; lean_object* v_str_3354_; lean_object* v_startInclusive_3355_; lean_object* v_endExclusive_3356_; lean_object* v___x_3357_; lean_object* v___x_3358_;
|
||||
v_head_3352_ = lean_ctor_get(v_x_3351_, 0);
|
||||
v_tail_3353_ = lean_ctor_get(v_x_3351_, 1);
|
||||
v_str_3354_ = lean_ctor_get(v_head_3352_, 0);
|
||||
v_startInclusive_3355_ = lean_ctor_get(v_head_3352_, 1);
|
||||
v_endExclusive_3356_ = lean_ctor_get(v_head_3352_, 2);
|
||||
v___x_3357_ = lean_string_utf8_extract(v_str_3354_, v_startInclusive_3355_, v_endExclusive_3356_);
|
||||
v___x_3358_ = lean_string_append(v_x_3350_, v___x_3357_);
|
||||
lean_dec_ref(v___x_3357_);
|
||||
v_x_3350_ = v___x_3358_;
|
||||
v_x_3351_ = v_tail_3353_;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_String_Slice_instToFormat___lam__0___boxed(lean_object* v_s_3361_){
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_List_foldl___at___00String_Slice_join_spec__0___boxed(lean_object* v_x_3360_, lean_object* v_x_3361_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_3362_;
|
||||
v_res_3362_ = l_String_Slice_instToFormat___lam__0(v_s_3361_);
|
||||
lean_dec_ref(v_s_3361_);
|
||||
v_res_3362_ = l_List_foldl___at___00String_Slice_join_spec__0(v_x_3360_, v_x_3361_);
|
||||
lean_dec(v_x_3361_);
|
||||
return v_res_3362_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_String_Slice_join(lean_object* v_l_3363_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_3364_; lean_object* v___x_3365_;
|
||||
v___x_3364_ = ((lean_object*)(l_String_Slice_replace___redArg___closed__1));
|
||||
v___x_3365_ = l_List_foldl___at___00String_Slice_join_spec__0(v___x_3364_, v_l_3363_);
|
||||
return v___x_3365_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_String_Slice_join___boxed(lean_object* v_l_3366_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_3367_;
|
||||
v_res_3367_ = l_String_Slice_join(v_l_3366_);
|
||||
lean_dec(v_l_3366_);
|
||||
return v_res_3367_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_String_Slice_toName(lean_object* v_s_3368_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_3369_; lean_object* v___x_3370_;
|
||||
v___x_3369_ = l_String_Slice_toString(v_s_3368_);
|
||||
v___x_3370_ = l_String_toName(v___x_3369_);
|
||||
return v___x_3370_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_String_Slice_toName___boxed(lean_object* v_s_3371_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_3372_;
|
||||
v_res_3372_ = l_String_Slice_toName(v_s_3371_);
|
||||
lean_dec_ref(v_s_3371_);
|
||||
return v_res_3372_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_String_Slice_instToFormat___lam__0(lean_object* v_s_3373_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_str_3374_; lean_object* v_startInclusive_3375_; lean_object* v_endExclusive_3376_; lean_object* v___x_3377_; lean_object* v___x_3378_;
|
||||
v_str_3374_ = lean_ctor_get(v_s_3373_, 0);
|
||||
v_startInclusive_3375_ = lean_ctor_get(v_s_3373_, 1);
|
||||
v_endExclusive_3376_ = lean_ctor_get(v_s_3373_, 2);
|
||||
v___x_3377_ = lean_string_utf8_extract(v_str_3374_, v_startInclusive_3375_, v_endExclusive_3376_);
|
||||
v___x_3378_ = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(v___x_3378_, 0, v___x_3377_);
|
||||
return v___x_3378_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_String_Slice_instToFormat___lam__0___boxed(lean_object* v_s_3379_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_3380_;
|
||||
v_res_3380_ = l_String_Slice_instToFormat___lam__0(v_s_3379_);
|
||||
lean_dec_ref(v_s_3379_);
|
||||
return v_res_3380_;
|
||||
}
|
||||
}
|
||||
lean_object* runtime_initialize_Init_Data_String_Pattern(uint8_t builtin);
|
||||
lean_object* runtime_initialize_Init_Data_Ord_Basic(uint8_t builtin);
|
||||
lean_object* runtime_initialize_Init_Data_Iterators_Combinators_FilterMap(uint8_t builtin);
|
||||
|
|
|
|||
7816
stage0/stdlib/Lake/Load/Lean/Eval.c
generated
7816
stage0/stdlib/Lake/Load/Lean/Eval.c
generated
File diff suppressed because it is too large
Load diff
8304
stage0/stdlib/Lake/Load/Toml.c
generated
8304
stage0/stdlib/Lake/Load/Toml.c
generated
File diff suppressed because it is too large
Load diff
4618
stage0/stdlib/Lake/Toml/Decode.c
generated
4618
stage0/stdlib/Lake/Toml/Decode.c
generated
File diff suppressed because it is too large
Load diff
8
stage0/stdlib/Lean/Compiler/LCNF/ExplicitRC.c
generated
8
stage0/stdlib/Lean/Compiler/LCNF/ExplicitRC.c
generated
|
|
@ -3050,7 +3050,7 @@ _start:
|
|||
lean_object* v___x_831_; lean_object* v___x_832_; lean_object* v___x_833_; lean_object* v___x_834_; lean_object* v___x_835_; lean_object* v___x_836_;
|
||||
v___x_831_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_CollectDerivedValInfo_collectCode___closed__6));
|
||||
v___x_832_ = lean_unsigned_to_nat(59u);
|
||||
v___x_833_ = lean_unsigned_to_nat(120u);
|
||||
v___x_833_ = lean_unsigned_to_nat(121u);
|
||||
v___x_834_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_CollectDerivedValInfo_collectCode___closed__5));
|
||||
v___x_835_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_CollectDerivedValInfo_collectCode___closed__4));
|
||||
v___x_836_ = l_mkPanicMessageWithDecl(v___x_835_, v___x_834_, v___x_833_, v___x_832_, v___x_831_);
|
||||
|
|
@ -7300,7 +7300,7 @@ _start:
|
|||
lean_object* v___x_2488_; lean_object* v___x_2489_; lean_object* v___x_2490_; lean_object* v___x_2491_; lean_object* v___x_2492_; lean_object* v___x_2493_;
|
||||
v___x_2488_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_CollectDerivedValInfo_collectCode___closed__6));
|
||||
v___x_2489_ = lean_unsigned_to_nat(20u);
|
||||
v___x_2490_ = lean_unsigned_to_nat(337u);
|
||||
v___x_2490_ = lean_unsigned_to_nat(338u);
|
||||
v___x_2491_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_useLetValue___closed__0));
|
||||
v___x_2492_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_CollectDerivedValInfo_collectCode___closed__4));
|
||||
v___x_2493_ = l_mkPanicMessageWithDecl(v___x_2492_, v___x_2491_, v___x_2490_, v___x_2489_, v___x_2488_);
|
||||
|
|
@ -10993,7 +10993,7 @@ _start:
|
|||
lean_object* v___x_4047_; lean_object* v___x_4048_; lean_object* v___x_4049_; lean_object* v___x_4050_; lean_object* v___x_4051_; lean_object* v___x_4052_;
|
||||
v___x_4047_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_CollectDerivedValInfo_collectCode___closed__6));
|
||||
v___x_4048_ = lean_unsigned_to_nat(22u);
|
||||
v___x_4049_ = lean_unsigned_to_nat(551u);
|
||||
v___x_4049_ = lean_unsigned_to_nat(552u);
|
||||
v___x_4050_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_LetDecl_explicitRc___closed__11));
|
||||
v___x_4051_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_CollectDerivedValInfo_collectCode___closed__4));
|
||||
v___x_4052_ = l_mkPanicMessageWithDecl(v___x_4051_, v___x_4050_, v___x_4049_, v___x_4048_, v___x_4047_);
|
||||
|
|
@ -13616,7 +13616,7 @@ _start:
|
|||
lean_object* v___x_4787_; lean_object* v___x_4788_; lean_object* v___x_4789_; lean_object* v___x_4790_; lean_object* v___x_4791_; lean_object* v___x_4792_;
|
||||
v___x_4787_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_CollectDerivedValInfo_collectCode___closed__6));
|
||||
v___x_4788_ = lean_unsigned_to_nat(59u);
|
||||
v___x_4789_ = lean_unsigned_to_nat(627u);
|
||||
v___x_4789_ = lean_unsigned_to_nat(628u);
|
||||
v___x_4790_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_Code_explicitRc___closed__0));
|
||||
v___x_4791_ = ((lean_object*)(l___private_Lean_Compiler_LCNF_ExplicitRC_0__Lean_Compiler_LCNF_CollectDerivedValInfo_collectCode___closed__4));
|
||||
v___x_4792_ = l_mkPanicMessageWithDecl(v___x_4791_, v___x_4790_, v___x_4789_, v___x_4788_, v___x_4787_);
|
||||
|
|
|
|||
4807
stage0/stdlib/Lean/Compiler/LCNF/InferBorrow.c
generated
4807
stage0/stdlib/Lean/Compiler/LCNF/InferBorrow.c
generated
File diff suppressed because it is too large
Load diff
6989
stage0/stdlib/Lean/Compiler/LCNF/PropagateBorrow.c
generated
6989
stage0/stdlib/Lean/Compiler/LCNF/PropagateBorrow.c
generated
File diff suppressed because it is too large
Load diff
10
stage0/stdlib/Lean/Declaration.c
generated
10
stage0/stdlib/Lean/Declaration.c
generated
|
|
@ -2847,7 +2847,7 @@ _start:
|
|||
lean_object* v___x_747_; lean_object* v___x_748_; lean_object* v___x_749_; lean_object* v___x_750_; lean_object* v___x_751_; lean_object* v___x_752_;
|
||||
v___x_747_ = ((lean_object*)(l_Lean_Declaration_definitionVal_x21___closed__2));
|
||||
v___x_748_ = lean_unsigned_to_nat(9u);
|
||||
v___x_749_ = lean_unsigned_to_nat(200u);
|
||||
v___x_749_ = lean_unsigned_to_nat(206u);
|
||||
v___x_750_ = ((lean_object*)(l_Lean_Declaration_definitionVal_x21___closed__1));
|
||||
v___x_751_ = ((lean_object*)(l_Lean_Declaration_definitionVal_x21___closed__0));
|
||||
v___x_752_ = l_mkPanicMessageWithDecl(v___x_751_, v___x_750_, v___x_749_, v___x_748_, v___x_747_);
|
||||
|
|
@ -5281,7 +5281,7 @@ _start:
|
|||
lean_object* v___x_1561_; lean_object* v___x_1562_; lean_object* v___x_1563_; lean_object* v___x_1564_; lean_object* v___x_1565_; lean_object* v___x_1566_;
|
||||
v___x_1561_ = ((lean_object*)(l_Lean_ConstantInfo_value_x21___closed__1));
|
||||
v___x_1562_ = lean_unsigned_to_nat(62u);
|
||||
v___x_1563_ = lean_unsigned_to_nat(502u);
|
||||
v___x_1563_ = lean_unsigned_to_nat(508u);
|
||||
v___x_1564_ = ((lean_object*)(l_Lean_ConstantInfo_value_x21___closed__0));
|
||||
v___x_1565_ = ((lean_object*)(l_Lean_Declaration_definitionVal_x21___closed__0));
|
||||
v___x_1566_ = l_mkPanicMessageWithDecl(v___x_1565_, v___x_1564_, v___x_1563_, v___x_1562_, v___x_1561_);
|
||||
|
|
@ -5294,7 +5294,7 @@ _start:
|
|||
lean_object* v___x_1567_; lean_object* v___x_1568_; lean_object* v___x_1569_; lean_object* v___x_1570_; lean_object* v___x_1571_; lean_object* v___x_1572_;
|
||||
v___x_1567_ = ((lean_object*)(l_Lean_ConstantInfo_value_x21___closed__1));
|
||||
v___x_1568_ = lean_unsigned_to_nat(62u);
|
||||
v___x_1569_ = lean_unsigned_to_nat(503u);
|
||||
v___x_1569_ = lean_unsigned_to_nat(509u);
|
||||
v___x_1570_ = ((lean_object*)(l_Lean_ConstantInfo_value_x21___closed__0));
|
||||
v___x_1571_ = ((lean_object*)(l_Lean_Declaration_definitionVal_x21___closed__0));
|
||||
v___x_1572_ = l_mkPanicMessageWithDecl(v___x_1571_, v___x_1570_, v___x_1569_, v___x_1568_, v___x_1567_);
|
||||
|
|
@ -5355,7 +5355,7 @@ default:
|
|||
lean_object* v___x_1587_; lean_object* v___x_1588_; lean_object* v___x_1589_; lean_object* v___x_1590_; lean_object* v___x_1591_; lean_object* v___x_1592_; uint8_t v___x_1593_; lean_object* v___x_1594_; lean_object* v___x_1595_; lean_object* v___x_1596_; lean_object* v___x_1597_; lean_object* v___x_1598_; lean_object* v___x_1599_;
|
||||
v___x_1587_ = ((lean_object*)(l_Lean_Declaration_definitionVal_x21___closed__0));
|
||||
v___x_1588_ = ((lean_object*)(l_Lean_ConstantInfo_value_x21___closed__0));
|
||||
v___x_1589_ = lean_unsigned_to_nat(504u);
|
||||
v___x_1589_ = lean_unsigned_to_nat(510u);
|
||||
v___x_1590_ = lean_unsigned_to_nat(31u);
|
||||
v___x_1591_ = ((lean_object*)(l_Lean_ConstantInfo_value_x21___closed__4));
|
||||
v___x_1592_ = l_Lean_ConstantInfo_name(v_info_1575_);
|
||||
|
|
@ -5561,7 +5561,7 @@ _start:
|
|||
lean_object* v___x_1645_; lean_object* v___x_1646_; lean_object* v___x_1647_; lean_object* v___x_1648_; lean_object* v___x_1649_; lean_object* v___x_1650_;
|
||||
v___x_1645_ = ((lean_object*)(l_Lean_ConstantInfo_inductiveVal_x21___closed__1));
|
||||
v___x_1646_ = lean_unsigned_to_nat(9u);
|
||||
v___x_1647_ = lean_unsigned_to_nat(532u);
|
||||
v___x_1647_ = lean_unsigned_to_nat(538u);
|
||||
v___x_1648_ = ((lean_object*)(l_Lean_ConstantInfo_inductiveVal_x21___closed__0));
|
||||
v___x_1649_ = ((lean_object*)(l_Lean_Declaration_definitionVal_x21___closed__0));
|
||||
v___x_1650_ = l_mkPanicMessageWithDecl(v___x_1649_, v___x_1648_, v___x_1647_, v___x_1646_, v___x_1645_);
|
||||
|
|
|
|||
23480
stage0/stdlib/Lean/Elab/BuiltinTerm.c
generated
23480
stage0/stdlib/Lean/Elab/BuiltinTerm.c
generated
File diff suppressed because it is too large
Load diff
18828
stage0/stdlib/Lean/Elab/Deriving/Basic.c
generated
18828
stage0/stdlib/Lean/Elab/Deriving/Basic.c
generated
File diff suppressed because it is too large
Load diff
1324
stage0/stdlib/Lean/Meta/Sym/AbstractS.c
generated
1324
stage0/stdlib/Lean/Meta/Sym/AbstractS.c
generated
File diff suppressed because it is too large
Load diff
4566
stage0/stdlib/Lean/Meta/Sym/AlphaShareBuilder.c
generated
4566
stage0/stdlib/Lean/Meta/Sym/AlphaShareBuilder.c
generated
File diff suppressed because it is too large
Load diff
742
stage0/stdlib/Lean/Meta/Sym/InferType.c
generated
742
stage0/stdlib/Lean/Meta/Sym/InferType.c
generated
File diff suppressed because it is too large
Load diff
10099
stage0/stdlib/Lean/Meta/Sym/InstantiateS.c
generated
10099
stage0/stdlib/Lean/Meta/Sym/InstantiateS.c
generated
File diff suppressed because it is too large
Load diff
2032
stage0/stdlib/Lean/Meta/Sym/LooseBVarsS.c
generated
2032
stage0/stdlib/Lean/Meta/Sym/LooseBVarsS.c
generated
File diff suppressed because it is too large
Load diff
4492
stage0/stdlib/Lean/Meta/Sym/MaxFVar.c
generated
4492
stage0/stdlib/Lean/Meta/Sym/MaxFVar.c
generated
File diff suppressed because it is too large
Load diff
11567
stage0/stdlib/Lean/Meta/Sym/Pattern.c
generated
11567
stage0/stdlib/Lean/Meta/Sym/Pattern.c
generated
File diff suppressed because it is too large
Load diff
297
stage0/stdlib/Lean/Meta/Sym/ProofInstInfo.c
generated
297
stage0/stdlib/Lean/Meta/Sym/ProofInstInfo.c
generated
|
|
@ -2045,10 +2045,10 @@ return v___x_741_;
|
|||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0___redArg___boxed(lean_object* v_x_742_, lean_object* v_x_743_, lean_object* v_x_744_){
|
||||
_start:
|
||||
{
|
||||
size_t v_x_2352__boxed_745_; lean_object* v_res_746_;
|
||||
v_x_2352__boxed_745_ = lean_unbox_usize(v_x_743_);
|
||||
size_t v_x_2373__boxed_745_; lean_object* v_res_746_;
|
||||
v_x_2373__boxed_745_ = lean_unbox_usize(v_x_743_);
|
||||
lean_dec(v_x_743_);
|
||||
v_res_746_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0___redArg(v_x_742_, v_x_2352__boxed_745_, v_x_744_);
|
||||
v_res_746_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0___redArg(v_x_742_, v_x_2373__boxed_745_, v_x_744_);
|
||||
lean_dec(v_x_744_);
|
||||
return v_res_746_;
|
||||
}
|
||||
|
|
@ -2583,12 +2583,12 @@ return v_res_898_;
|
|||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2___redArg___boxed(lean_object* v_x_899_, lean_object* v_x_900_, lean_object* v_x_901_, lean_object* v_x_902_, lean_object* v_x_903_){
|
||||
_start:
|
||||
{
|
||||
size_t v_x_2526__boxed_904_; size_t v_x_2527__boxed_905_; lean_object* v_res_906_;
|
||||
v_x_2526__boxed_904_ = lean_unbox_usize(v_x_900_);
|
||||
size_t v_x_2547__boxed_904_; size_t v_x_2548__boxed_905_; lean_object* v_res_906_;
|
||||
v_x_2547__boxed_904_ = lean_unbox_usize(v_x_900_);
|
||||
lean_dec(v_x_900_);
|
||||
v_x_2527__boxed_905_ = lean_unbox_usize(v_x_901_);
|
||||
v_x_2548__boxed_905_ = lean_unbox_usize(v_x_901_);
|
||||
lean_dec(v_x_901_);
|
||||
v_res_906_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2___redArg(v_x_899_, v_x_2526__boxed_904_, v_x_2527__boxed_905_, v_x_902_, v_x_903_);
|
||||
v_res_906_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2___redArg(v_x_899_, v_x_2547__boxed_904_, v_x_2548__boxed_905_, v_x_902_, v_x_903_);
|
||||
return v_res_906_;
|
||||
}
|
||||
}
|
||||
|
|
@ -2680,13 +2680,13 @@ lean_inc(v_declName_917_);
|
|||
v___x_935_ = l_Lean_Meta_Sym_mkProofInstInfo_x3f(v_declName_917_, v_a_919_, v_a_920_, v_a_921_, v_a_922_);
|
||||
if (lean_obj_tag(v___x_935_) == 0)
|
||||
{
|
||||
lean_object* v_a_936_; lean_object* v___x_938_; uint8_t v_isShared_939_; uint8_t v_isSharedCheck_961_;
|
||||
lean_object* v_a_936_; lean_object* v___x_938_; uint8_t v_isShared_939_; uint8_t v_isSharedCheck_962_;
|
||||
v_a_936_ = lean_ctor_get(v___x_935_, 0);
|
||||
v_isSharedCheck_961_ = !lean_is_exclusive(v___x_935_);
|
||||
if (v_isSharedCheck_961_ == 0)
|
||||
v_isSharedCheck_962_ = !lean_is_exclusive(v___x_935_);
|
||||
if (v_isSharedCheck_962_ == 0)
|
||||
{
|
||||
v___x_938_ = v___x_935_;
|
||||
v_isShared_939_ = v_isSharedCheck_961_;
|
||||
v_isShared_939_ = v_isSharedCheck_962_;
|
||||
goto v_resetjp_937_;
|
||||
}
|
||||
else
|
||||
|
|
@ -2694,12 +2694,12 @@ else
|
|||
lean_inc(v_a_936_);
|
||||
lean_dec(v___x_935_);
|
||||
v___x_938_ = lean_box(0);
|
||||
v_isShared_939_ = v_isSharedCheck_961_;
|
||||
v_isShared_939_ = v_isSharedCheck_962_;
|
||||
goto v_resetjp_937_;
|
||||
}
|
||||
v_resetjp_937_:
|
||||
{
|
||||
lean_object* v___x_940_; lean_object* v_share_941_; lean_object* v_maxFVar_942_; lean_object* v_proofInstInfo_943_; lean_object* v_inferType_944_; lean_object* v_getLevel_945_; lean_object* v_congrInfo_946_; lean_object* v_defEqI_947_; uint8_t v_debug_948_; lean_object* v___x_950_; uint8_t v_isShared_951_; uint8_t v_isSharedCheck_960_;
|
||||
lean_object* v___x_940_; lean_object* v_share_941_; lean_object* v_maxFVar_942_; lean_object* v_proofInstInfo_943_; lean_object* v_inferType_944_; lean_object* v_getLevel_945_; lean_object* v_congrInfo_946_; lean_object* v_defEqI_947_; lean_object* v_extensions_948_; uint8_t v_debug_949_; lean_object* v___x_951_; uint8_t v_isShared_952_; uint8_t v_isSharedCheck_961_;
|
||||
v___x_940_ = lean_st_ref_take(v_a_918_);
|
||||
v_share_941_ = lean_ctor_get(v___x_940_, 0);
|
||||
v_maxFVar_942_ = lean_ctor_get(v___x_940_, 1);
|
||||
|
|
@ -2708,16 +2708,18 @@ v_inferType_944_ = lean_ctor_get(v___x_940_, 3);
|
|||
v_getLevel_945_ = lean_ctor_get(v___x_940_, 4);
|
||||
v_congrInfo_946_ = lean_ctor_get(v___x_940_, 5);
|
||||
v_defEqI_947_ = lean_ctor_get(v___x_940_, 6);
|
||||
v_debug_948_ = lean_ctor_get_uint8(v___x_940_, sizeof(void*)*7);
|
||||
v_isSharedCheck_960_ = !lean_is_exclusive(v___x_940_);
|
||||
if (v_isSharedCheck_960_ == 0)
|
||||
v_extensions_948_ = lean_ctor_get(v___x_940_, 7);
|
||||
v_debug_949_ = lean_ctor_get_uint8(v___x_940_, sizeof(void*)*8);
|
||||
v_isSharedCheck_961_ = !lean_is_exclusive(v___x_940_);
|
||||
if (v_isSharedCheck_961_ == 0)
|
||||
{
|
||||
v___x_950_ = v___x_940_;
|
||||
v_isShared_951_ = v_isSharedCheck_960_;
|
||||
goto v_resetjp_949_;
|
||||
v___x_951_ = v___x_940_;
|
||||
v_isShared_952_ = v_isSharedCheck_961_;
|
||||
goto v_resetjp_950_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_extensions_948_);
|
||||
lean_inc(v_defEqI_947_);
|
||||
lean_inc(v_congrInfo_946_);
|
||||
lean_inc(v_getLevel_945_);
|
||||
|
|
@ -2726,56 +2728,57 @@ lean_inc(v_proofInstInfo_943_);
|
|||
lean_inc(v_maxFVar_942_);
|
||||
lean_inc(v_share_941_);
|
||||
lean_dec(v___x_940_);
|
||||
v___x_950_ = lean_box(0);
|
||||
v_isShared_951_ = v_isSharedCheck_960_;
|
||||
goto v_resetjp_949_;
|
||||
v___x_951_ = lean_box(0);
|
||||
v_isShared_952_ = v_isSharedCheck_961_;
|
||||
goto v_resetjp_950_;
|
||||
}
|
||||
v_resetjp_949_:
|
||||
v_resetjp_950_:
|
||||
{
|
||||
lean_object* v___x_952_; lean_object* v___x_954_;
|
||||
lean_object* v___x_953_; lean_object* v___x_955_;
|
||||
lean_inc(v_a_936_);
|
||||
v___x_952_ = l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1___redArg(v_proofInstInfo_943_, v_declName_917_, v_a_936_);
|
||||
if (v_isShared_951_ == 0)
|
||||
v___x_953_ = l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1___redArg(v_proofInstInfo_943_, v_declName_917_, v_a_936_);
|
||||
if (v_isShared_952_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_950_, 2, v___x_952_);
|
||||
v___x_954_ = v___x_950_;
|
||||
goto v_reusejp_953_;
|
||||
lean_ctor_set(v___x_951_, 2, v___x_953_);
|
||||
v___x_955_ = v___x_951_;
|
||||
goto v_reusejp_954_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_960_;
|
||||
v_reuseFailAlloc_960_ = lean_alloc_ctor(0, 8, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_960_, 0, v_share_941_);
|
||||
lean_ctor_set(v_reuseFailAlloc_960_, 1, v_maxFVar_942_);
|
||||
lean_ctor_set(v_reuseFailAlloc_960_, 2, v___x_953_);
|
||||
lean_ctor_set(v_reuseFailAlloc_960_, 3, v_inferType_944_);
|
||||
lean_ctor_set(v_reuseFailAlloc_960_, 4, v_getLevel_945_);
|
||||
lean_ctor_set(v_reuseFailAlloc_960_, 5, v_congrInfo_946_);
|
||||
lean_ctor_set(v_reuseFailAlloc_960_, 6, v_defEqI_947_);
|
||||
lean_ctor_set(v_reuseFailAlloc_960_, 7, v_extensions_948_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_960_, sizeof(void*)*8, v_debug_949_);
|
||||
v___x_955_ = v_reuseFailAlloc_960_;
|
||||
goto v_reusejp_954_;
|
||||
}
|
||||
v_reusejp_954_:
|
||||
{
|
||||
lean_object* v___x_956_; lean_object* v___x_958_;
|
||||
v___x_956_ = lean_st_ref_set(v_a_918_, v___x_955_);
|
||||
if (v_isShared_939_ == 0)
|
||||
{
|
||||
v___x_958_ = v___x_938_;
|
||||
goto v_reusejp_957_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_959_;
|
||||
v_reuseFailAlloc_959_ = lean_alloc_ctor(0, 7, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_959_, 0, v_share_941_);
|
||||
lean_ctor_set(v_reuseFailAlloc_959_, 1, v_maxFVar_942_);
|
||||
lean_ctor_set(v_reuseFailAlloc_959_, 2, v___x_952_);
|
||||
lean_ctor_set(v_reuseFailAlloc_959_, 3, v_inferType_944_);
|
||||
lean_ctor_set(v_reuseFailAlloc_959_, 4, v_getLevel_945_);
|
||||
lean_ctor_set(v_reuseFailAlloc_959_, 5, v_congrInfo_946_);
|
||||
lean_ctor_set(v_reuseFailAlloc_959_, 6, v_defEqI_947_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_959_, sizeof(void*)*7, v_debug_948_);
|
||||
v___x_954_ = v_reuseFailAlloc_959_;
|
||||
goto v_reusejp_953_;
|
||||
v_reuseFailAlloc_959_ = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(v_reuseFailAlloc_959_, 0, v_a_936_);
|
||||
v___x_958_ = v_reuseFailAlloc_959_;
|
||||
goto v_reusejp_957_;
|
||||
}
|
||||
v_reusejp_953_:
|
||||
v_reusejp_957_:
|
||||
{
|
||||
lean_object* v___x_955_; lean_object* v___x_957_;
|
||||
v___x_955_ = lean_st_ref_set(v_a_918_, v___x_954_);
|
||||
if (v_isShared_939_ == 0)
|
||||
{
|
||||
v___x_957_ = v___x_938_;
|
||||
goto v_reusejp_956_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_958_;
|
||||
v_reuseFailAlloc_958_ = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(v_reuseFailAlloc_958_, 0, v_a_936_);
|
||||
v___x_957_ = v_reuseFailAlloc_958_;
|
||||
goto v_reusejp_956_;
|
||||
}
|
||||
v_reusejp_956_:
|
||||
{
|
||||
return v___x_957_;
|
||||
return v___x_958_;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -2789,158 +2792,158 @@ return v___x_935_;
|
|||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getProofInstInfo_x3f___redArg___boxed(lean_object* v_declName_962_, lean_object* v_a_963_, lean_object* v_a_964_, lean_object* v_a_965_, lean_object* v_a_966_, lean_object* v_a_967_, lean_object* v_a_968_){
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getProofInstInfo_x3f___redArg___boxed(lean_object* v_declName_963_, lean_object* v_a_964_, lean_object* v_a_965_, lean_object* v_a_966_, lean_object* v_a_967_, lean_object* v_a_968_, lean_object* v_a_969_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_969_;
|
||||
v_res_969_ = l_Lean_Meta_Sym_getProofInstInfo_x3f___redArg(v_declName_962_, v_a_963_, v_a_964_, v_a_965_, v_a_966_, v_a_967_);
|
||||
lean_dec(v_a_967_);
|
||||
lean_dec_ref(v_a_966_);
|
||||
lean_dec(v_a_965_);
|
||||
lean_dec_ref(v_a_964_);
|
||||
lean_dec(v_a_963_);
|
||||
return v_res_969_;
|
||||
lean_object* v_res_970_;
|
||||
v_res_970_ = l_Lean_Meta_Sym_getProofInstInfo_x3f___redArg(v_declName_963_, v_a_964_, v_a_965_, v_a_966_, v_a_967_, v_a_968_);
|
||||
lean_dec(v_a_968_);
|
||||
lean_dec_ref(v_a_967_);
|
||||
lean_dec(v_a_966_);
|
||||
lean_dec_ref(v_a_965_);
|
||||
lean_dec(v_a_964_);
|
||||
return v_res_970_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getProofInstInfo_x3f(lean_object* v_declName_970_, lean_object* v_a_971_, lean_object* v_a_972_, lean_object* v_a_973_, lean_object* v_a_974_, lean_object* v_a_975_, lean_object* v_a_976_){
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getProofInstInfo_x3f(lean_object* v_declName_971_, lean_object* v_a_972_, lean_object* v_a_973_, lean_object* v_a_974_, lean_object* v_a_975_, lean_object* v_a_976_, lean_object* v_a_977_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_978_;
|
||||
v___x_978_ = l_Lean_Meta_Sym_getProofInstInfo_x3f___redArg(v_declName_970_, v_a_972_, v_a_973_, v_a_974_, v_a_975_, v_a_976_);
|
||||
return v___x_978_;
|
||||
lean_object* v___x_979_;
|
||||
v___x_979_ = l_Lean_Meta_Sym_getProofInstInfo_x3f___redArg(v_declName_971_, v_a_973_, v_a_974_, v_a_975_, v_a_976_, v_a_977_);
|
||||
return v___x_979_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getProofInstInfo_x3f___boxed(lean_object* v_declName_979_, lean_object* v_a_980_, lean_object* v_a_981_, lean_object* v_a_982_, lean_object* v_a_983_, lean_object* v_a_984_, lean_object* v_a_985_, lean_object* v_a_986_){
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getProofInstInfo_x3f___boxed(lean_object* v_declName_980_, lean_object* v_a_981_, lean_object* v_a_982_, lean_object* v_a_983_, lean_object* v_a_984_, lean_object* v_a_985_, lean_object* v_a_986_, lean_object* v_a_987_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_987_;
|
||||
v_res_987_ = l_Lean_Meta_Sym_getProofInstInfo_x3f(v_declName_979_, v_a_980_, v_a_981_, v_a_982_, v_a_983_, v_a_984_, v_a_985_);
|
||||
lean_dec(v_a_985_);
|
||||
lean_dec_ref(v_a_984_);
|
||||
lean_dec(v_a_983_);
|
||||
lean_dec_ref(v_a_982_);
|
||||
lean_dec(v_a_981_);
|
||||
lean_dec_ref(v_a_980_);
|
||||
return v_res_987_;
|
||||
lean_object* v_res_988_;
|
||||
v_res_988_ = l_Lean_Meta_Sym_getProofInstInfo_x3f(v_declName_980_, v_a_981_, v_a_982_, v_a_983_, v_a_984_, v_a_985_, v_a_986_);
|
||||
lean_dec(v_a_986_);
|
||||
lean_dec_ref(v_a_985_);
|
||||
lean_dec(v_a_984_);
|
||||
lean_dec_ref(v_a_983_);
|
||||
lean_dec(v_a_982_);
|
||||
lean_dec_ref(v_a_981_);
|
||||
return v_res_988_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0(lean_object* v_00_u03b2_988_, lean_object* v_x_989_, lean_object* v_x_990_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0(lean_object* v_00_u03b2_989_, lean_object* v_x_990_, lean_object* v_x_991_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_991_;
|
||||
v___x_991_ = l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0___redArg(v_x_989_, v_x_990_);
|
||||
return v___x_991_;
|
||||
lean_object* v___x_992_;
|
||||
v___x_992_ = l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0___redArg(v_x_990_, v_x_991_);
|
||||
return v___x_992_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0___boxed(lean_object* v_00_u03b2_992_, lean_object* v_x_993_, lean_object* v_x_994_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0___boxed(lean_object* v_00_u03b2_993_, lean_object* v_x_994_, lean_object* v_x_995_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_995_;
|
||||
v_res_995_ = l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0(v_00_u03b2_992_, v_x_993_, v_x_994_);
|
||||
lean_dec(v_x_994_);
|
||||
return v_res_995_;
|
||||
lean_object* v_res_996_;
|
||||
v_res_996_ = l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0(v_00_u03b2_993_, v_x_994_, v_x_995_);
|
||||
lean_dec(v_x_995_);
|
||||
return v_res_996_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1(lean_object* v_00_u03b2_996_, lean_object* v_x_997_, lean_object* v_x_998_, lean_object* v_x_999_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1(lean_object* v_00_u03b2_997_, lean_object* v_x_998_, lean_object* v_x_999_, lean_object* v_x_1000_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_1000_;
|
||||
v___x_1000_ = l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1___redArg(v_x_997_, v_x_998_, v_x_999_);
|
||||
return v___x_1000_;
|
||||
lean_object* v___x_1001_;
|
||||
v___x_1001_ = l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1___redArg(v_x_998_, v_x_999_, v_x_1000_);
|
||||
return v___x_1001_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0(lean_object* v_00_u03b2_1001_, lean_object* v_x_1002_, size_t v_x_1003_, lean_object* v_x_1004_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0(lean_object* v_00_u03b2_1002_, lean_object* v_x_1003_, size_t v_x_1004_, lean_object* v_x_1005_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_1005_;
|
||||
v___x_1005_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0___redArg(v_x_1002_, v_x_1003_, v_x_1004_);
|
||||
return v___x_1005_;
|
||||
lean_object* v___x_1006_;
|
||||
v___x_1006_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0___redArg(v_x_1003_, v_x_1004_, v_x_1005_);
|
||||
return v___x_1006_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0___boxed(lean_object* v_00_u03b2_1006_, lean_object* v_x_1007_, lean_object* v_x_1008_, lean_object* v_x_1009_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0___boxed(lean_object* v_00_u03b2_1007_, lean_object* v_x_1008_, lean_object* v_x_1009_, lean_object* v_x_1010_){
|
||||
_start:
|
||||
{
|
||||
size_t v_x_2788__boxed_1010_; lean_object* v_res_1011_;
|
||||
v_x_2788__boxed_1010_ = lean_unbox_usize(v_x_1008_);
|
||||
lean_dec(v_x_1008_);
|
||||
v_res_1011_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0(v_00_u03b2_1006_, v_x_1007_, v_x_2788__boxed_1010_, v_x_1009_);
|
||||
size_t v_x_2809__boxed_1011_; lean_object* v_res_1012_;
|
||||
v_x_2809__boxed_1011_ = lean_unbox_usize(v_x_1009_);
|
||||
lean_dec(v_x_1009_);
|
||||
return v_res_1011_;
|
||||
v_res_1012_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0(v_00_u03b2_1007_, v_x_1008_, v_x_2809__boxed_1011_, v_x_1010_);
|
||||
lean_dec(v_x_1010_);
|
||||
return v_res_1012_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2(lean_object* v_00_u03b2_1012_, lean_object* v_x_1013_, size_t v_x_1014_, size_t v_x_1015_, lean_object* v_x_1016_, lean_object* v_x_1017_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2(lean_object* v_00_u03b2_1013_, lean_object* v_x_1014_, size_t v_x_1015_, size_t v_x_1016_, lean_object* v_x_1017_, lean_object* v_x_1018_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_1018_;
|
||||
v___x_1018_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2___redArg(v_x_1013_, v_x_1014_, v_x_1015_, v_x_1016_, v_x_1017_);
|
||||
return v___x_1018_;
|
||||
lean_object* v___x_1019_;
|
||||
v___x_1019_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2___redArg(v_x_1014_, v_x_1015_, v_x_1016_, v_x_1017_, v_x_1018_);
|
||||
return v___x_1019_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2___boxed(lean_object* v_00_u03b2_1019_, lean_object* v_x_1020_, lean_object* v_x_1021_, lean_object* v_x_1022_, lean_object* v_x_1023_, lean_object* v_x_1024_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2___boxed(lean_object* v_00_u03b2_1020_, lean_object* v_x_1021_, lean_object* v_x_1022_, lean_object* v_x_1023_, lean_object* v_x_1024_, lean_object* v_x_1025_){
|
||||
_start:
|
||||
{
|
||||
size_t v_x_2799__boxed_1025_; size_t v_x_2800__boxed_1026_; lean_object* v_res_1027_;
|
||||
v_x_2799__boxed_1025_ = lean_unbox_usize(v_x_1021_);
|
||||
lean_dec(v_x_1021_);
|
||||
v_x_2800__boxed_1026_ = lean_unbox_usize(v_x_1022_);
|
||||
size_t v_x_2820__boxed_1026_; size_t v_x_2821__boxed_1027_; lean_object* v_res_1028_;
|
||||
v_x_2820__boxed_1026_ = lean_unbox_usize(v_x_1022_);
|
||||
lean_dec(v_x_1022_);
|
||||
v_res_1027_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2(v_00_u03b2_1019_, v_x_1020_, v_x_2799__boxed_1025_, v_x_2800__boxed_1026_, v_x_1023_, v_x_1024_);
|
||||
return v_res_1027_;
|
||||
v_x_2821__boxed_1027_ = lean_unbox_usize(v_x_1023_);
|
||||
lean_dec(v_x_1023_);
|
||||
v_res_1028_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2(v_00_u03b2_1020_, v_x_1021_, v_x_2820__boxed_1026_, v_x_2821__boxed_1027_, v_x_1024_, v_x_1025_);
|
||||
return v_res_1028_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0_spec__1(lean_object* v_00_u03b2_1028_, lean_object* v_keys_1029_, lean_object* v_vals_1030_, lean_object* v_heq_1031_, lean_object* v_i_1032_, lean_object* v_k_1033_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0_spec__1(lean_object* v_00_u03b2_1029_, lean_object* v_keys_1030_, lean_object* v_vals_1031_, lean_object* v_heq_1032_, lean_object* v_i_1033_, lean_object* v_k_1034_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_1034_;
|
||||
v___x_1034_ = l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0_spec__1___redArg(v_keys_1029_, v_vals_1030_, v_i_1032_, v_k_1033_);
|
||||
return v___x_1034_;
|
||||
lean_object* v___x_1035_;
|
||||
v___x_1035_ = l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0_spec__1___redArg(v_keys_1030_, v_vals_1031_, v_i_1033_, v_k_1034_);
|
||||
return v___x_1035_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0_spec__1___boxed(lean_object* v_00_u03b2_1035_, lean_object* v_keys_1036_, lean_object* v_vals_1037_, lean_object* v_heq_1038_, lean_object* v_i_1039_, lean_object* v_k_1040_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0_spec__1___boxed(lean_object* v_00_u03b2_1036_, lean_object* v_keys_1037_, lean_object* v_vals_1038_, lean_object* v_heq_1039_, lean_object* v_i_1040_, lean_object* v_k_1041_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_1041_;
|
||||
v_res_1041_ = l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0_spec__1(v_00_u03b2_1035_, v_keys_1036_, v_vals_1037_, v_heq_1038_, v_i_1039_, v_k_1040_);
|
||||
lean_dec(v_k_1040_);
|
||||
lean_dec_ref(v_vals_1037_);
|
||||
lean_dec_ref(v_keys_1036_);
|
||||
return v_res_1041_;
|
||||
lean_object* v_res_1042_;
|
||||
v_res_1042_ = l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__0_spec__0_spec__1(v_00_u03b2_1036_, v_keys_1037_, v_vals_1038_, v_heq_1039_, v_i_1040_, v_k_1041_);
|
||||
lean_dec(v_k_1041_);
|
||||
lean_dec_ref(v_vals_1038_);
|
||||
lean_dec_ref(v_keys_1037_);
|
||||
return v_res_1042_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__4(lean_object* v_00_u03b2_1042_, lean_object* v_n_1043_, lean_object* v_k_1044_, lean_object* v_v_1045_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__4(lean_object* v_00_u03b2_1043_, lean_object* v_n_1044_, lean_object* v_k_1045_, lean_object* v_v_1046_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_1046_;
|
||||
v___x_1046_ = l_Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__4___redArg(v_n_1043_, v_k_1044_, v_v_1045_);
|
||||
return v___x_1046_;
|
||||
lean_object* v___x_1047_;
|
||||
v___x_1047_ = l_Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__4___redArg(v_n_1044_, v_k_1045_, v_v_1046_);
|
||||
return v___x_1047_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__5(lean_object* v_00_u03b2_1047_, size_t v_depth_1048_, lean_object* v_keys_1049_, lean_object* v_vals_1050_, lean_object* v_heq_1051_, lean_object* v_i_1052_, lean_object* v_entries_1053_){
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__5(lean_object* v_00_u03b2_1048_, size_t v_depth_1049_, lean_object* v_keys_1050_, lean_object* v_vals_1051_, lean_object* v_heq_1052_, lean_object* v_i_1053_, lean_object* v_entries_1054_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_1054_;
|
||||
v___x_1054_ = l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__5___redArg(v_depth_1048_, v_keys_1049_, v_vals_1050_, v_i_1052_, v_entries_1053_);
|
||||
return v___x_1054_;
|
||||
lean_object* v___x_1055_;
|
||||
v___x_1055_ = l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__5___redArg(v_depth_1049_, v_keys_1050_, v_vals_1051_, v_i_1053_, v_entries_1054_);
|
||||
return v___x_1055_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__5___boxed(lean_object* v_00_u03b2_1055_, lean_object* v_depth_1056_, lean_object* v_keys_1057_, lean_object* v_vals_1058_, lean_object* v_heq_1059_, lean_object* v_i_1060_, lean_object* v_entries_1061_){
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__5___boxed(lean_object* v_00_u03b2_1056_, lean_object* v_depth_1057_, lean_object* v_keys_1058_, lean_object* v_vals_1059_, lean_object* v_heq_1060_, lean_object* v_i_1061_, lean_object* v_entries_1062_){
|
||||
_start:
|
||||
{
|
||||
size_t v_depth_boxed_1062_; lean_object* v_res_1063_;
|
||||
v_depth_boxed_1062_ = lean_unbox_usize(v_depth_1056_);
|
||||
lean_dec(v_depth_1056_);
|
||||
v_res_1063_ = l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__5(v_00_u03b2_1055_, v_depth_boxed_1062_, v_keys_1057_, v_vals_1058_, v_heq_1059_, v_i_1060_, v_entries_1061_);
|
||||
lean_dec_ref(v_vals_1058_);
|
||||
lean_dec_ref(v_keys_1057_);
|
||||
return v_res_1063_;
|
||||
size_t v_depth_boxed_1063_; lean_object* v_res_1064_;
|
||||
v_depth_boxed_1063_ = lean_unbox_usize(v_depth_1057_);
|
||||
lean_dec(v_depth_1057_);
|
||||
v_res_1064_ = l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__5(v_00_u03b2_1056_, v_depth_boxed_1063_, v_keys_1058_, v_vals_1059_, v_heq_1060_, v_i_1061_, v_entries_1062_);
|
||||
lean_dec_ref(v_vals_1059_);
|
||||
lean_dec_ref(v_keys_1058_);
|
||||
return v_res_1064_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at___00Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__4_spec__5(lean_object* v_00_u03b2_1064_, lean_object* v_x_1065_, lean_object* v_x_1066_, lean_object* v_x_1067_, lean_object* v_x_1068_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at___00Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__4_spec__5(lean_object* v_00_u03b2_1065_, lean_object* v_x_1066_, lean_object* v_x_1067_, lean_object* v_x_1068_, lean_object* v_x_1069_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_1069_;
|
||||
v___x_1069_ = l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at___00Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__4_spec__5___redArg(v_x_1065_, v_x_1066_, v_x_1067_, v_x_1068_);
|
||||
return v___x_1069_;
|
||||
lean_object* v___x_1070_;
|
||||
v___x_1070_ = l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at___00Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getProofInstInfo_x3f_spec__1_spec__2_spec__4_spec__5___redArg(v_x_1066_, v_x_1067_, v_x_1068_, v_x_1069_);
|
||||
return v___x_1070_;
|
||||
}
|
||||
}
|
||||
lean_object* runtime_initialize_Lean_Meta_Sym_SymM(uint8_t builtin);
|
||||
|
|
|
|||
880
stage0/stdlib/Lean/Meta/Sym/ReplaceS.c
generated
880
stage0/stdlib/Lean/Meta/Sym/ReplaceS.c
generated
|
|
@ -3273,7 +3273,7 @@ return v___x_855_;
|
|||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_replaceS___redArg(lean_object* v_e_856_, lean_object* v_f_857_, lean_object* v_a_858_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_860_; lean_object* v_share_861_; lean_object* v_maxFVar_862_; lean_object* v_proofInstInfo_863_; lean_object* v_inferType_864_; lean_object* v_getLevel_865_; lean_object* v_congrInfo_866_; lean_object* v_defEqI_867_; uint8_t v_debug_868_; lean_object* v___x_870_; uint8_t v_isShared_871_; uint8_t v_isSharedCheck_918_;
|
||||
lean_object* v___x_860_; lean_object* v_share_861_; lean_object* v_maxFVar_862_; lean_object* v_proofInstInfo_863_; lean_object* v_inferType_864_; lean_object* v_getLevel_865_; lean_object* v_congrInfo_866_; lean_object* v_defEqI_867_; lean_object* v_extensions_868_; uint8_t v_debug_869_; lean_object* v___x_871_; uint8_t v_isShared_872_; uint8_t v_isSharedCheck_920_;
|
||||
v___x_860_ = lean_st_ref_take(v_a_858_);
|
||||
v_share_861_ = lean_ctor_get(v___x_860_, 0);
|
||||
v_maxFVar_862_ = lean_ctor_get(v___x_860_, 1);
|
||||
|
|
@ -3282,16 +3282,18 @@ v_inferType_864_ = lean_ctor_get(v___x_860_, 3);
|
|||
v_getLevel_865_ = lean_ctor_get(v___x_860_, 4);
|
||||
v_congrInfo_866_ = lean_ctor_get(v___x_860_, 5);
|
||||
v_defEqI_867_ = lean_ctor_get(v___x_860_, 6);
|
||||
v_debug_868_ = lean_ctor_get_uint8(v___x_860_, sizeof(void*)*7);
|
||||
v_isSharedCheck_918_ = !lean_is_exclusive(v___x_860_);
|
||||
if (v_isSharedCheck_918_ == 0)
|
||||
v_extensions_868_ = lean_ctor_get(v___x_860_, 7);
|
||||
v_debug_869_ = lean_ctor_get_uint8(v___x_860_, sizeof(void*)*8);
|
||||
v_isSharedCheck_920_ = !lean_is_exclusive(v___x_860_);
|
||||
if (v_isSharedCheck_920_ == 0)
|
||||
{
|
||||
v___x_870_ = v___x_860_;
|
||||
v_isShared_871_ = v_isSharedCheck_918_;
|
||||
goto v_resetjp_869_;
|
||||
v___x_871_ = v___x_860_;
|
||||
v_isShared_872_ = v_isSharedCheck_920_;
|
||||
goto v_resetjp_870_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_extensions_868_);
|
||||
lean_inc(v_defEqI_867_);
|
||||
lean_inc(v_congrInfo_866_);
|
||||
lean_inc(v_getLevel_865_);
|
||||
|
|
@ -3300,484 +3302,226 @@ lean_inc(v_proofInstInfo_863_);
|
|||
lean_inc(v_maxFVar_862_);
|
||||
lean_inc(v_share_861_);
|
||||
lean_dec(v___x_860_);
|
||||
v___x_870_ = lean_box(0);
|
||||
v_isShared_871_ = v_isSharedCheck_918_;
|
||||
goto v_resetjp_869_;
|
||||
v___x_871_ = lean_box(0);
|
||||
v_isShared_872_ = v_isSharedCheck_920_;
|
||||
goto v_resetjp_870_;
|
||||
}
|
||||
v_resetjp_869_:
|
||||
v_resetjp_870_:
|
||||
{
|
||||
lean_object* v___x_872_; lean_object* v___x_874_;
|
||||
v___x_872_ = lean_obj_once(&l_Lean_Meta_Sym_replaceS___redArg___closed__2, &l_Lean_Meta_Sym_replaceS___redArg___closed__2_once, _init_l_Lean_Meta_Sym_replaceS___redArg___closed__2);
|
||||
if (v_isShared_871_ == 0)
|
||||
lean_object* v___x_873_; lean_object* v___x_875_;
|
||||
v___x_873_ = lean_obj_once(&l_Lean_Meta_Sym_replaceS___redArg___closed__2, &l_Lean_Meta_Sym_replaceS___redArg___closed__2_once, _init_l_Lean_Meta_Sym_replaceS___redArg___closed__2);
|
||||
if (v_isShared_872_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_870_, 0, v___x_872_);
|
||||
v___x_874_ = v___x_870_;
|
||||
goto v_reusejp_873_;
|
||||
lean_ctor_set(v___x_871_, 0, v___x_873_);
|
||||
v___x_875_ = v___x_871_;
|
||||
goto v_reusejp_874_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_917_;
|
||||
v_reuseFailAlloc_917_ = lean_alloc_ctor(0, 7, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_917_, 0, v___x_872_);
|
||||
lean_ctor_set(v_reuseFailAlloc_917_, 1, v_maxFVar_862_);
|
||||
lean_ctor_set(v_reuseFailAlloc_917_, 2, v_proofInstInfo_863_);
|
||||
lean_ctor_set(v_reuseFailAlloc_917_, 3, v_inferType_864_);
|
||||
lean_ctor_set(v_reuseFailAlloc_917_, 4, v_getLevel_865_);
|
||||
lean_ctor_set(v_reuseFailAlloc_917_, 5, v_congrInfo_866_);
|
||||
lean_ctor_set(v_reuseFailAlloc_917_, 6, v_defEqI_867_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_917_, sizeof(void*)*7, v_debug_868_);
|
||||
v___x_874_ = v_reuseFailAlloc_917_;
|
||||
goto v_reusejp_873_;
|
||||
lean_object* v_reuseFailAlloc_919_;
|
||||
v_reuseFailAlloc_919_ = lean_alloc_ctor(0, 8, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_919_, 0, v___x_873_);
|
||||
lean_ctor_set(v_reuseFailAlloc_919_, 1, v_maxFVar_862_);
|
||||
lean_ctor_set(v_reuseFailAlloc_919_, 2, v_proofInstInfo_863_);
|
||||
lean_ctor_set(v_reuseFailAlloc_919_, 3, v_inferType_864_);
|
||||
lean_ctor_set(v_reuseFailAlloc_919_, 4, v_getLevel_865_);
|
||||
lean_ctor_set(v_reuseFailAlloc_919_, 5, v_congrInfo_866_);
|
||||
lean_ctor_set(v_reuseFailAlloc_919_, 6, v_defEqI_867_);
|
||||
lean_ctor_set(v_reuseFailAlloc_919_, 7, v_extensions_868_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_919_, sizeof(void*)*8, v_debug_869_);
|
||||
v___x_875_ = v_reuseFailAlloc_919_;
|
||||
goto v_reusejp_874_;
|
||||
}
|
||||
v_reusejp_873_:
|
||||
v_reusejp_874_:
|
||||
{
|
||||
lean_object* v___x_875_; lean_object* v___x_876_; lean_object* v_fst_878_; lean_object* v_snd_879_; uint8_t v_debug_898_; lean_object* v___x_899_; lean_object* v___x_900_; lean_object* v___x_901_; lean_object* v_fst_902_;
|
||||
v___x_875_ = lean_st_ref_set(v_a_858_, v___x_874_);
|
||||
v___x_876_ = lean_st_ref_get(v_a_858_);
|
||||
v_debug_898_ = lean_ctor_get_uint8(v___x_876_, sizeof(void*)*7);
|
||||
lean_dec(v___x_876_);
|
||||
v___x_899_ = lean_unsigned_to_nat(0u);
|
||||
v___x_900_ = lean_box(v_debug_898_);
|
||||
lean_object* v___x_876_; lean_object* v___x_877_; lean_object* v_fst_879_; lean_object* v_snd_880_; uint8_t v_debug_900_; lean_object* v___x_901_; lean_object* v___x_902_; lean_object* v___x_903_; lean_object* v_fst_904_;
|
||||
v___x_876_ = lean_st_ref_set(v_a_858_, v___x_875_);
|
||||
v___x_877_ = lean_st_ref_get(v_a_858_);
|
||||
v_debug_900_ = lean_ctor_get_uint8(v___x_877_, sizeof(void*)*8);
|
||||
lean_dec(v___x_877_);
|
||||
v___x_901_ = lean_unsigned_to_nat(0u);
|
||||
v___x_902_ = lean_box(v_debug_900_);
|
||||
lean_inc_ref(v_f_857_);
|
||||
lean_inc_ref(v_e_856_);
|
||||
v___x_901_ = lean_apply_4(v_f_857_, v_e_856_, v___x_899_, v___x_900_, v_share_861_);
|
||||
v_fst_902_ = lean_ctor_get(v___x_901_, 0);
|
||||
lean_inc(v_fst_902_);
|
||||
if (lean_obj_tag(v_fst_902_) == 1)
|
||||
v___x_903_ = lean_apply_4(v_f_857_, v_e_856_, v___x_901_, v___x_902_, v_share_861_);
|
||||
v_fst_904_ = lean_ctor_get(v___x_903_, 0);
|
||||
lean_inc(v_fst_904_);
|
||||
if (lean_obj_tag(v_fst_904_) == 1)
|
||||
{
|
||||
lean_object* v_snd_903_; lean_object* v_val_904_;
|
||||
lean_object* v_snd_905_; lean_object* v_val_906_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
lean_dec_ref(v_e_856_);
|
||||
v_snd_903_ = lean_ctor_get(v___x_901_, 1);
|
||||
lean_inc(v_snd_903_);
|
||||
lean_dec_ref(v___x_901_);
|
||||
v_val_904_ = lean_ctor_get(v_fst_902_, 0);
|
||||
lean_inc(v_val_904_);
|
||||
lean_dec_ref(v_fst_902_);
|
||||
v_fst_878_ = v_val_904_;
|
||||
v_snd_879_ = v_snd_903_;
|
||||
goto v___jp_877_;
|
||||
v_snd_905_ = lean_ctor_get(v___x_903_, 1);
|
||||
lean_inc(v_snd_905_);
|
||||
lean_dec_ref(v___x_903_);
|
||||
v_val_906_ = lean_ctor_get(v_fst_904_, 0);
|
||||
lean_inc(v_val_906_);
|
||||
lean_dec_ref(v_fst_904_);
|
||||
v_fst_879_ = v_val_906_;
|
||||
v_snd_880_ = v_snd_905_;
|
||||
goto v___jp_878_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(v_fst_902_);
|
||||
lean_dec(v_fst_904_);
|
||||
switch(lean_obj_tag(v_e_856_))
|
||||
{
|
||||
case 9:
|
||||
{
|
||||
lean_object* v_snd_905_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
v_snd_905_ = lean_ctor_get(v___x_901_, 1);
|
||||
lean_inc(v_snd_905_);
|
||||
lean_dec_ref(v___x_901_);
|
||||
v_fst_878_ = v_e_856_;
|
||||
v_snd_879_ = v_snd_905_;
|
||||
goto v___jp_877_;
|
||||
}
|
||||
case 2:
|
||||
{
|
||||
lean_object* v_snd_906_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
v_snd_906_ = lean_ctor_get(v___x_901_, 1);
|
||||
lean_inc(v_snd_906_);
|
||||
lean_dec_ref(v___x_901_);
|
||||
v_fst_878_ = v_e_856_;
|
||||
v_snd_879_ = v_snd_906_;
|
||||
goto v___jp_877_;
|
||||
}
|
||||
case 0:
|
||||
{
|
||||
lean_object* v_snd_907_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
v_snd_907_ = lean_ctor_get(v___x_901_, 1);
|
||||
v_snd_907_ = lean_ctor_get(v___x_903_, 1);
|
||||
lean_inc(v_snd_907_);
|
||||
lean_dec_ref(v___x_901_);
|
||||
v_fst_878_ = v_e_856_;
|
||||
v_snd_879_ = v_snd_907_;
|
||||
goto v___jp_877_;
|
||||
lean_dec_ref(v___x_903_);
|
||||
v_fst_879_ = v_e_856_;
|
||||
v_snd_880_ = v_snd_907_;
|
||||
goto v___jp_878_;
|
||||
}
|
||||
case 1:
|
||||
case 2:
|
||||
{
|
||||
lean_object* v_snd_908_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
v_snd_908_ = lean_ctor_get(v___x_901_, 1);
|
||||
v_snd_908_ = lean_ctor_get(v___x_903_, 1);
|
||||
lean_inc(v_snd_908_);
|
||||
lean_dec_ref(v___x_901_);
|
||||
v_fst_878_ = v_e_856_;
|
||||
v_snd_879_ = v_snd_908_;
|
||||
goto v___jp_877_;
|
||||
}
|
||||
case 4:
|
||||
{
|
||||
lean_object* v_snd_909_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
v_snd_909_ = lean_ctor_get(v___x_901_, 1);
|
||||
lean_inc(v_snd_909_);
|
||||
lean_dec_ref(v___x_901_);
|
||||
v_fst_878_ = v_e_856_;
|
||||
v_snd_879_ = v_snd_909_;
|
||||
goto v___jp_877_;
|
||||
}
|
||||
case 3:
|
||||
{
|
||||
lean_object* v_snd_910_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
v_snd_910_ = lean_ctor_get(v___x_901_, 1);
|
||||
lean_inc(v_snd_910_);
|
||||
lean_dec_ref(v___x_901_);
|
||||
v_fst_878_ = v_e_856_;
|
||||
v_snd_879_ = v_snd_910_;
|
||||
goto v___jp_877_;
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* v_snd_911_; lean_object* v___x_912_; lean_object* v___x_913_; lean_object* v_fst_914_; lean_object* v_snd_915_; lean_object* v_fst_916_;
|
||||
v_snd_911_ = lean_ctor_get(v___x_901_, 1);
|
||||
lean_inc(v_snd_911_);
|
||||
lean_dec_ref(v___x_901_);
|
||||
v___x_912_ = lean_obj_once(&l_Lean_Meta_Sym_replaceS_x27___closed__1, &l_Lean_Meta_Sym_replaceS_x27___closed__1_once, _init_l_Lean_Meta_Sym_replaceS_x27___closed__1);
|
||||
v___x_913_ = l___private_Lean_Meta_Sym_ReplaceS_0__Lean_Meta_Sym_visit(v_e_856_, v___x_899_, v_f_857_, v___x_912_, v_debug_898_, v_snd_911_);
|
||||
v_fst_914_ = lean_ctor_get(v___x_913_, 0);
|
||||
lean_inc(v_fst_914_);
|
||||
v_snd_915_ = lean_ctor_get(v___x_913_, 1);
|
||||
lean_inc(v_snd_915_);
|
||||
lean_dec_ref(v___x_913_);
|
||||
v_fst_916_ = lean_ctor_get(v_fst_914_, 0);
|
||||
lean_inc(v_fst_916_);
|
||||
lean_dec(v_fst_914_);
|
||||
v_fst_878_ = v_fst_916_;
|
||||
v_snd_879_ = v_snd_915_;
|
||||
goto v___jp_877_;
|
||||
}
|
||||
}
|
||||
}
|
||||
v___jp_877_:
|
||||
{
|
||||
lean_object* v___x_880_; lean_object* v_maxFVar_881_; lean_object* v_proofInstInfo_882_; lean_object* v_inferType_883_; lean_object* v_getLevel_884_; lean_object* v_congrInfo_885_; lean_object* v_defEqI_886_; uint8_t v_debug_887_; lean_object* v___x_889_; uint8_t v_isShared_890_; uint8_t v_isSharedCheck_896_;
|
||||
v___x_880_ = lean_st_ref_take(v_a_858_);
|
||||
v_maxFVar_881_ = lean_ctor_get(v___x_880_, 1);
|
||||
v_proofInstInfo_882_ = lean_ctor_get(v___x_880_, 2);
|
||||
v_inferType_883_ = lean_ctor_get(v___x_880_, 3);
|
||||
v_getLevel_884_ = lean_ctor_get(v___x_880_, 4);
|
||||
v_congrInfo_885_ = lean_ctor_get(v___x_880_, 5);
|
||||
v_defEqI_886_ = lean_ctor_get(v___x_880_, 6);
|
||||
v_debug_887_ = lean_ctor_get_uint8(v___x_880_, sizeof(void*)*7);
|
||||
v_isSharedCheck_896_ = !lean_is_exclusive(v___x_880_);
|
||||
if (v_isSharedCheck_896_ == 0)
|
||||
{
|
||||
lean_object* v_unused_897_;
|
||||
v_unused_897_ = lean_ctor_get(v___x_880_, 0);
|
||||
lean_dec(v_unused_897_);
|
||||
v___x_889_ = v___x_880_;
|
||||
v_isShared_890_ = v_isSharedCheck_896_;
|
||||
goto v_resetjp_888_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_defEqI_886_);
|
||||
lean_inc(v_congrInfo_885_);
|
||||
lean_inc(v_getLevel_884_);
|
||||
lean_inc(v_inferType_883_);
|
||||
lean_inc(v_proofInstInfo_882_);
|
||||
lean_inc(v_maxFVar_881_);
|
||||
lean_dec(v___x_880_);
|
||||
v___x_889_ = lean_box(0);
|
||||
v_isShared_890_ = v_isSharedCheck_896_;
|
||||
goto v_resetjp_888_;
|
||||
}
|
||||
v_resetjp_888_:
|
||||
{
|
||||
lean_object* v___x_892_;
|
||||
if (v_isShared_890_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_889_, 0, v_snd_879_);
|
||||
v___x_892_ = v___x_889_;
|
||||
goto v_reusejp_891_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_895_;
|
||||
v_reuseFailAlloc_895_ = lean_alloc_ctor(0, 7, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_895_, 0, v_snd_879_);
|
||||
lean_ctor_set(v_reuseFailAlloc_895_, 1, v_maxFVar_881_);
|
||||
lean_ctor_set(v_reuseFailAlloc_895_, 2, v_proofInstInfo_882_);
|
||||
lean_ctor_set(v_reuseFailAlloc_895_, 3, v_inferType_883_);
|
||||
lean_ctor_set(v_reuseFailAlloc_895_, 4, v_getLevel_884_);
|
||||
lean_ctor_set(v_reuseFailAlloc_895_, 5, v_congrInfo_885_);
|
||||
lean_ctor_set(v_reuseFailAlloc_895_, 6, v_defEqI_886_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_895_, sizeof(void*)*7, v_debug_887_);
|
||||
v___x_892_ = v_reuseFailAlloc_895_;
|
||||
goto v_reusejp_891_;
|
||||
}
|
||||
v_reusejp_891_:
|
||||
{
|
||||
lean_object* v___x_893_; lean_object* v___x_894_;
|
||||
v___x_893_ = lean_st_ref_set(v_a_858_, v___x_892_);
|
||||
v___x_894_ = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(v___x_894_, 0, v_fst_878_);
|
||||
return v___x_894_;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_replaceS___redArg___boxed(lean_object* v_e_919_, lean_object* v_f_920_, lean_object* v_a_921_, lean_object* v_a_922_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_923_;
|
||||
v_res_923_ = l_Lean_Meta_Sym_replaceS___redArg(v_e_919_, v_f_920_, v_a_921_);
|
||||
lean_dec(v_a_921_);
|
||||
return v_res_923_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_replaceS(lean_object* v_e_924_, lean_object* v_f_925_, lean_object* v_a_926_, lean_object* v_a_927_, lean_object* v_a_928_, lean_object* v_a_929_, lean_object* v_a_930_, lean_object* v_a_931_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_933_; lean_object* v_share_934_; lean_object* v_maxFVar_935_; lean_object* v_proofInstInfo_936_; lean_object* v_inferType_937_; lean_object* v_getLevel_938_; lean_object* v_congrInfo_939_; lean_object* v_defEqI_940_; uint8_t v_debug_941_; lean_object* v___x_943_; uint8_t v_isShared_944_; uint8_t v_isSharedCheck_991_;
|
||||
v___x_933_ = lean_st_ref_take(v_a_927_);
|
||||
v_share_934_ = lean_ctor_get(v___x_933_, 0);
|
||||
v_maxFVar_935_ = lean_ctor_get(v___x_933_, 1);
|
||||
v_proofInstInfo_936_ = lean_ctor_get(v___x_933_, 2);
|
||||
v_inferType_937_ = lean_ctor_get(v___x_933_, 3);
|
||||
v_getLevel_938_ = lean_ctor_get(v___x_933_, 4);
|
||||
v_congrInfo_939_ = lean_ctor_get(v___x_933_, 5);
|
||||
v_defEqI_940_ = lean_ctor_get(v___x_933_, 6);
|
||||
v_debug_941_ = lean_ctor_get_uint8(v___x_933_, sizeof(void*)*7);
|
||||
v_isSharedCheck_991_ = !lean_is_exclusive(v___x_933_);
|
||||
if (v_isSharedCheck_991_ == 0)
|
||||
{
|
||||
v___x_943_ = v___x_933_;
|
||||
v_isShared_944_ = v_isSharedCheck_991_;
|
||||
goto v_resetjp_942_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_defEqI_940_);
|
||||
lean_inc(v_congrInfo_939_);
|
||||
lean_inc(v_getLevel_938_);
|
||||
lean_inc(v_inferType_937_);
|
||||
lean_inc(v_proofInstInfo_936_);
|
||||
lean_inc(v_maxFVar_935_);
|
||||
lean_inc(v_share_934_);
|
||||
lean_dec(v___x_933_);
|
||||
v___x_943_ = lean_box(0);
|
||||
v_isShared_944_ = v_isSharedCheck_991_;
|
||||
goto v_resetjp_942_;
|
||||
}
|
||||
v_resetjp_942_:
|
||||
{
|
||||
lean_object* v___x_945_; lean_object* v___x_947_;
|
||||
v___x_945_ = lean_obj_once(&l_Lean_Meta_Sym_replaceS___redArg___closed__2, &l_Lean_Meta_Sym_replaceS___redArg___closed__2_once, _init_l_Lean_Meta_Sym_replaceS___redArg___closed__2);
|
||||
if (v_isShared_944_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_943_, 0, v___x_945_);
|
||||
v___x_947_ = v___x_943_;
|
||||
goto v_reusejp_946_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_990_;
|
||||
v_reuseFailAlloc_990_ = lean_alloc_ctor(0, 7, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_990_, 0, v___x_945_);
|
||||
lean_ctor_set(v_reuseFailAlloc_990_, 1, v_maxFVar_935_);
|
||||
lean_ctor_set(v_reuseFailAlloc_990_, 2, v_proofInstInfo_936_);
|
||||
lean_ctor_set(v_reuseFailAlloc_990_, 3, v_inferType_937_);
|
||||
lean_ctor_set(v_reuseFailAlloc_990_, 4, v_getLevel_938_);
|
||||
lean_ctor_set(v_reuseFailAlloc_990_, 5, v_congrInfo_939_);
|
||||
lean_ctor_set(v_reuseFailAlloc_990_, 6, v_defEqI_940_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_990_, sizeof(void*)*7, v_debug_941_);
|
||||
v___x_947_ = v_reuseFailAlloc_990_;
|
||||
goto v_reusejp_946_;
|
||||
}
|
||||
v_reusejp_946_:
|
||||
{
|
||||
lean_object* v___x_948_; lean_object* v___x_949_; lean_object* v_fst_951_; lean_object* v_snd_952_; uint8_t v_debug_971_; lean_object* v___x_972_; lean_object* v___x_973_; lean_object* v___x_974_; lean_object* v_fst_975_;
|
||||
v___x_948_ = lean_st_ref_set(v_a_927_, v___x_947_);
|
||||
v___x_949_ = lean_st_ref_get(v_a_927_);
|
||||
v_debug_971_ = lean_ctor_get_uint8(v___x_949_, sizeof(void*)*7);
|
||||
lean_dec(v___x_949_);
|
||||
v___x_972_ = lean_unsigned_to_nat(0u);
|
||||
v___x_973_ = lean_box(v_debug_971_);
|
||||
lean_inc_ref(v_f_925_);
|
||||
lean_inc_ref(v_e_924_);
|
||||
v___x_974_ = lean_apply_4(v_f_925_, v_e_924_, v___x_972_, v___x_973_, v_share_934_);
|
||||
v_fst_975_ = lean_ctor_get(v___x_974_, 0);
|
||||
lean_inc(v_fst_975_);
|
||||
if (lean_obj_tag(v_fst_975_) == 1)
|
||||
{
|
||||
lean_object* v_snd_976_; lean_object* v_val_977_;
|
||||
lean_dec_ref(v_f_925_);
|
||||
lean_dec_ref(v_e_924_);
|
||||
v_snd_976_ = lean_ctor_get(v___x_974_, 1);
|
||||
lean_inc(v_snd_976_);
|
||||
lean_dec_ref(v___x_974_);
|
||||
v_val_977_ = lean_ctor_get(v_fst_975_, 0);
|
||||
lean_inc(v_val_977_);
|
||||
lean_dec_ref(v_fst_975_);
|
||||
v_fst_951_ = v_val_977_;
|
||||
v_snd_952_ = v_snd_976_;
|
||||
goto v___jp_950_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(v_fst_975_);
|
||||
switch(lean_obj_tag(v_e_924_))
|
||||
{
|
||||
case 9:
|
||||
{
|
||||
lean_object* v_snd_978_;
|
||||
lean_dec_ref(v_f_925_);
|
||||
v_snd_978_ = lean_ctor_get(v___x_974_, 1);
|
||||
lean_inc(v_snd_978_);
|
||||
lean_dec_ref(v___x_974_);
|
||||
v_fst_951_ = v_e_924_;
|
||||
v_snd_952_ = v_snd_978_;
|
||||
goto v___jp_950_;
|
||||
}
|
||||
case 2:
|
||||
{
|
||||
lean_object* v_snd_979_;
|
||||
lean_dec_ref(v_f_925_);
|
||||
v_snd_979_ = lean_ctor_get(v___x_974_, 1);
|
||||
lean_inc(v_snd_979_);
|
||||
lean_dec_ref(v___x_974_);
|
||||
v_fst_951_ = v_e_924_;
|
||||
v_snd_952_ = v_snd_979_;
|
||||
goto v___jp_950_;
|
||||
lean_dec_ref(v___x_903_);
|
||||
v_fst_879_ = v_e_856_;
|
||||
v_snd_880_ = v_snd_908_;
|
||||
goto v___jp_878_;
|
||||
}
|
||||
case 0:
|
||||
{
|
||||
lean_object* v_snd_980_;
|
||||
lean_dec_ref(v_f_925_);
|
||||
v_snd_980_ = lean_ctor_get(v___x_974_, 1);
|
||||
lean_inc(v_snd_980_);
|
||||
lean_dec_ref(v___x_974_);
|
||||
v_fst_951_ = v_e_924_;
|
||||
v_snd_952_ = v_snd_980_;
|
||||
goto v___jp_950_;
|
||||
lean_object* v_snd_909_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
v_snd_909_ = lean_ctor_get(v___x_903_, 1);
|
||||
lean_inc(v_snd_909_);
|
||||
lean_dec_ref(v___x_903_);
|
||||
v_fst_879_ = v_e_856_;
|
||||
v_snd_880_ = v_snd_909_;
|
||||
goto v___jp_878_;
|
||||
}
|
||||
case 1:
|
||||
{
|
||||
lean_object* v_snd_981_;
|
||||
lean_dec_ref(v_f_925_);
|
||||
v_snd_981_ = lean_ctor_get(v___x_974_, 1);
|
||||
lean_inc(v_snd_981_);
|
||||
lean_dec_ref(v___x_974_);
|
||||
v_fst_951_ = v_e_924_;
|
||||
v_snd_952_ = v_snd_981_;
|
||||
goto v___jp_950_;
|
||||
lean_object* v_snd_910_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
v_snd_910_ = lean_ctor_get(v___x_903_, 1);
|
||||
lean_inc(v_snd_910_);
|
||||
lean_dec_ref(v___x_903_);
|
||||
v_fst_879_ = v_e_856_;
|
||||
v_snd_880_ = v_snd_910_;
|
||||
goto v___jp_878_;
|
||||
}
|
||||
case 4:
|
||||
{
|
||||
lean_object* v_snd_982_;
|
||||
lean_dec_ref(v_f_925_);
|
||||
v_snd_982_ = lean_ctor_get(v___x_974_, 1);
|
||||
lean_inc(v_snd_982_);
|
||||
lean_dec_ref(v___x_974_);
|
||||
v_fst_951_ = v_e_924_;
|
||||
v_snd_952_ = v_snd_982_;
|
||||
goto v___jp_950_;
|
||||
lean_object* v_snd_911_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
v_snd_911_ = lean_ctor_get(v___x_903_, 1);
|
||||
lean_inc(v_snd_911_);
|
||||
lean_dec_ref(v___x_903_);
|
||||
v_fst_879_ = v_e_856_;
|
||||
v_snd_880_ = v_snd_911_;
|
||||
goto v___jp_878_;
|
||||
}
|
||||
case 3:
|
||||
{
|
||||
lean_object* v_snd_983_;
|
||||
lean_dec_ref(v_f_925_);
|
||||
v_snd_983_ = lean_ctor_get(v___x_974_, 1);
|
||||
lean_inc(v_snd_983_);
|
||||
lean_dec_ref(v___x_974_);
|
||||
v_fst_951_ = v_e_924_;
|
||||
v_snd_952_ = v_snd_983_;
|
||||
goto v___jp_950_;
|
||||
lean_object* v_snd_912_;
|
||||
lean_dec_ref(v_f_857_);
|
||||
v_snd_912_ = lean_ctor_get(v___x_903_, 1);
|
||||
lean_inc(v_snd_912_);
|
||||
lean_dec_ref(v___x_903_);
|
||||
v_fst_879_ = v_e_856_;
|
||||
v_snd_880_ = v_snd_912_;
|
||||
goto v___jp_878_;
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* v_snd_984_; lean_object* v___x_985_; lean_object* v___x_986_; lean_object* v_fst_987_; lean_object* v_snd_988_; lean_object* v_fst_989_;
|
||||
v_snd_984_ = lean_ctor_get(v___x_974_, 1);
|
||||
lean_inc(v_snd_984_);
|
||||
lean_dec_ref(v___x_974_);
|
||||
v___x_985_ = lean_obj_once(&l_Lean_Meta_Sym_replaceS_x27___closed__1, &l_Lean_Meta_Sym_replaceS_x27___closed__1_once, _init_l_Lean_Meta_Sym_replaceS_x27___closed__1);
|
||||
v___x_986_ = l___private_Lean_Meta_Sym_ReplaceS_0__Lean_Meta_Sym_visit(v_e_924_, v___x_972_, v_f_925_, v___x_985_, v_debug_971_, v_snd_984_);
|
||||
v_fst_987_ = lean_ctor_get(v___x_986_, 0);
|
||||
lean_inc(v_fst_987_);
|
||||
v_snd_988_ = lean_ctor_get(v___x_986_, 1);
|
||||
lean_inc(v_snd_988_);
|
||||
lean_dec_ref(v___x_986_);
|
||||
v_fst_989_ = lean_ctor_get(v_fst_987_, 0);
|
||||
lean_inc(v_fst_989_);
|
||||
lean_dec(v_fst_987_);
|
||||
v_fst_951_ = v_fst_989_;
|
||||
v_snd_952_ = v_snd_988_;
|
||||
goto v___jp_950_;
|
||||
lean_object* v_snd_913_; lean_object* v___x_914_; lean_object* v___x_915_; lean_object* v_fst_916_; lean_object* v_snd_917_; lean_object* v_fst_918_;
|
||||
v_snd_913_ = lean_ctor_get(v___x_903_, 1);
|
||||
lean_inc(v_snd_913_);
|
||||
lean_dec_ref(v___x_903_);
|
||||
v___x_914_ = lean_obj_once(&l_Lean_Meta_Sym_replaceS_x27___closed__1, &l_Lean_Meta_Sym_replaceS_x27___closed__1_once, _init_l_Lean_Meta_Sym_replaceS_x27___closed__1);
|
||||
v___x_915_ = l___private_Lean_Meta_Sym_ReplaceS_0__Lean_Meta_Sym_visit(v_e_856_, v___x_901_, v_f_857_, v___x_914_, v_debug_900_, v_snd_913_);
|
||||
v_fst_916_ = lean_ctor_get(v___x_915_, 0);
|
||||
lean_inc(v_fst_916_);
|
||||
v_snd_917_ = lean_ctor_get(v___x_915_, 1);
|
||||
lean_inc(v_snd_917_);
|
||||
lean_dec_ref(v___x_915_);
|
||||
v_fst_918_ = lean_ctor_get(v_fst_916_, 0);
|
||||
lean_inc(v_fst_918_);
|
||||
lean_dec(v_fst_916_);
|
||||
v_fst_879_ = v_fst_918_;
|
||||
v_snd_880_ = v_snd_917_;
|
||||
goto v___jp_878_;
|
||||
}
|
||||
}
|
||||
}
|
||||
v___jp_950_:
|
||||
v___jp_878_:
|
||||
{
|
||||
lean_object* v___x_953_; lean_object* v_maxFVar_954_; lean_object* v_proofInstInfo_955_; lean_object* v_inferType_956_; lean_object* v_getLevel_957_; lean_object* v_congrInfo_958_; lean_object* v_defEqI_959_; uint8_t v_debug_960_; lean_object* v___x_962_; uint8_t v_isShared_963_; uint8_t v_isSharedCheck_969_;
|
||||
v___x_953_ = lean_st_ref_take(v_a_927_);
|
||||
v_maxFVar_954_ = lean_ctor_get(v___x_953_, 1);
|
||||
v_proofInstInfo_955_ = lean_ctor_get(v___x_953_, 2);
|
||||
v_inferType_956_ = lean_ctor_get(v___x_953_, 3);
|
||||
v_getLevel_957_ = lean_ctor_get(v___x_953_, 4);
|
||||
v_congrInfo_958_ = lean_ctor_get(v___x_953_, 5);
|
||||
v_defEqI_959_ = lean_ctor_get(v___x_953_, 6);
|
||||
v_debug_960_ = lean_ctor_get_uint8(v___x_953_, sizeof(void*)*7);
|
||||
v_isSharedCheck_969_ = !lean_is_exclusive(v___x_953_);
|
||||
if (v_isSharedCheck_969_ == 0)
|
||||
lean_object* v___x_881_; lean_object* v_maxFVar_882_; lean_object* v_proofInstInfo_883_; lean_object* v_inferType_884_; lean_object* v_getLevel_885_; lean_object* v_congrInfo_886_; lean_object* v_defEqI_887_; lean_object* v_extensions_888_; uint8_t v_debug_889_; lean_object* v___x_891_; uint8_t v_isShared_892_; uint8_t v_isSharedCheck_898_;
|
||||
v___x_881_ = lean_st_ref_take(v_a_858_);
|
||||
v_maxFVar_882_ = lean_ctor_get(v___x_881_, 1);
|
||||
v_proofInstInfo_883_ = lean_ctor_get(v___x_881_, 2);
|
||||
v_inferType_884_ = lean_ctor_get(v___x_881_, 3);
|
||||
v_getLevel_885_ = lean_ctor_get(v___x_881_, 4);
|
||||
v_congrInfo_886_ = lean_ctor_get(v___x_881_, 5);
|
||||
v_defEqI_887_ = lean_ctor_get(v___x_881_, 6);
|
||||
v_extensions_888_ = lean_ctor_get(v___x_881_, 7);
|
||||
v_debug_889_ = lean_ctor_get_uint8(v___x_881_, sizeof(void*)*8);
|
||||
v_isSharedCheck_898_ = !lean_is_exclusive(v___x_881_);
|
||||
if (v_isSharedCheck_898_ == 0)
|
||||
{
|
||||
lean_object* v_unused_970_;
|
||||
v_unused_970_ = lean_ctor_get(v___x_953_, 0);
|
||||
lean_dec(v_unused_970_);
|
||||
v___x_962_ = v___x_953_;
|
||||
v_isShared_963_ = v_isSharedCheck_969_;
|
||||
goto v_resetjp_961_;
|
||||
lean_object* v_unused_899_;
|
||||
v_unused_899_ = lean_ctor_get(v___x_881_, 0);
|
||||
lean_dec(v_unused_899_);
|
||||
v___x_891_ = v___x_881_;
|
||||
v_isShared_892_ = v_isSharedCheck_898_;
|
||||
goto v_resetjp_890_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_defEqI_959_);
|
||||
lean_inc(v_congrInfo_958_);
|
||||
lean_inc(v_getLevel_957_);
|
||||
lean_inc(v_inferType_956_);
|
||||
lean_inc(v_proofInstInfo_955_);
|
||||
lean_inc(v_maxFVar_954_);
|
||||
lean_dec(v___x_953_);
|
||||
v___x_962_ = lean_box(0);
|
||||
v_isShared_963_ = v_isSharedCheck_969_;
|
||||
goto v_resetjp_961_;
|
||||
lean_inc(v_extensions_888_);
|
||||
lean_inc(v_defEqI_887_);
|
||||
lean_inc(v_congrInfo_886_);
|
||||
lean_inc(v_getLevel_885_);
|
||||
lean_inc(v_inferType_884_);
|
||||
lean_inc(v_proofInstInfo_883_);
|
||||
lean_inc(v_maxFVar_882_);
|
||||
lean_dec(v___x_881_);
|
||||
v___x_891_ = lean_box(0);
|
||||
v_isShared_892_ = v_isSharedCheck_898_;
|
||||
goto v_resetjp_890_;
|
||||
}
|
||||
v_resetjp_961_:
|
||||
v_resetjp_890_:
|
||||
{
|
||||
lean_object* v___x_965_;
|
||||
if (v_isShared_963_ == 0)
|
||||
lean_object* v___x_894_;
|
||||
if (v_isShared_892_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_962_, 0, v_snd_952_);
|
||||
v___x_965_ = v___x_962_;
|
||||
goto v_reusejp_964_;
|
||||
lean_ctor_set(v___x_891_, 0, v_snd_880_);
|
||||
v___x_894_ = v___x_891_;
|
||||
goto v_reusejp_893_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_968_;
|
||||
v_reuseFailAlloc_968_ = lean_alloc_ctor(0, 7, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_968_, 0, v_snd_952_);
|
||||
lean_ctor_set(v_reuseFailAlloc_968_, 1, v_maxFVar_954_);
|
||||
lean_ctor_set(v_reuseFailAlloc_968_, 2, v_proofInstInfo_955_);
|
||||
lean_ctor_set(v_reuseFailAlloc_968_, 3, v_inferType_956_);
|
||||
lean_ctor_set(v_reuseFailAlloc_968_, 4, v_getLevel_957_);
|
||||
lean_ctor_set(v_reuseFailAlloc_968_, 5, v_congrInfo_958_);
|
||||
lean_ctor_set(v_reuseFailAlloc_968_, 6, v_defEqI_959_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_968_, sizeof(void*)*7, v_debug_960_);
|
||||
v___x_965_ = v_reuseFailAlloc_968_;
|
||||
goto v_reusejp_964_;
|
||||
lean_object* v_reuseFailAlloc_897_;
|
||||
v_reuseFailAlloc_897_ = lean_alloc_ctor(0, 8, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_897_, 0, v_snd_880_);
|
||||
lean_ctor_set(v_reuseFailAlloc_897_, 1, v_maxFVar_882_);
|
||||
lean_ctor_set(v_reuseFailAlloc_897_, 2, v_proofInstInfo_883_);
|
||||
lean_ctor_set(v_reuseFailAlloc_897_, 3, v_inferType_884_);
|
||||
lean_ctor_set(v_reuseFailAlloc_897_, 4, v_getLevel_885_);
|
||||
lean_ctor_set(v_reuseFailAlloc_897_, 5, v_congrInfo_886_);
|
||||
lean_ctor_set(v_reuseFailAlloc_897_, 6, v_defEqI_887_);
|
||||
lean_ctor_set(v_reuseFailAlloc_897_, 7, v_extensions_888_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_897_, sizeof(void*)*8, v_debug_889_);
|
||||
v___x_894_ = v_reuseFailAlloc_897_;
|
||||
goto v_reusejp_893_;
|
||||
}
|
||||
v_reusejp_964_:
|
||||
v_reusejp_893_:
|
||||
{
|
||||
lean_object* v___x_966_; lean_object* v___x_967_;
|
||||
v___x_966_ = lean_st_ref_set(v_a_927_, v___x_965_);
|
||||
v___x_967_ = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(v___x_967_, 0, v_fst_951_);
|
||||
return v___x_967_;
|
||||
lean_object* v___x_895_; lean_object* v___x_896_;
|
||||
v___x_895_ = lean_st_ref_set(v_a_858_, v___x_894_);
|
||||
v___x_896_ = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(v___x_896_, 0, v_fst_879_);
|
||||
return v___x_896_;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -3785,18 +3529,286 @@ return v___x_967_;
|
|||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_replaceS___boxed(lean_object* v_e_992_, lean_object* v_f_993_, lean_object* v_a_994_, lean_object* v_a_995_, lean_object* v_a_996_, lean_object* v_a_997_, lean_object* v_a_998_, lean_object* v_a_999_, lean_object* v_a_1000_){
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_replaceS___redArg___boxed(lean_object* v_e_921_, lean_object* v_f_922_, lean_object* v_a_923_, lean_object* v_a_924_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_1001_;
|
||||
v_res_1001_ = l_Lean_Meta_Sym_replaceS(v_e_992_, v_f_993_, v_a_994_, v_a_995_, v_a_996_, v_a_997_, v_a_998_, v_a_999_);
|
||||
lean_object* v_res_925_;
|
||||
v_res_925_ = l_Lean_Meta_Sym_replaceS___redArg(v_e_921_, v_f_922_, v_a_923_);
|
||||
lean_dec(v_a_923_);
|
||||
return v_res_925_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_replaceS(lean_object* v_e_926_, lean_object* v_f_927_, lean_object* v_a_928_, lean_object* v_a_929_, lean_object* v_a_930_, lean_object* v_a_931_, lean_object* v_a_932_, lean_object* v_a_933_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_935_; lean_object* v_share_936_; lean_object* v_maxFVar_937_; lean_object* v_proofInstInfo_938_; lean_object* v_inferType_939_; lean_object* v_getLevel_940_; lean_object* v_congrInfo_941_; lean_object* v_defEqI_942_; lean_object* v_extensions_943_; uint8_t v_debug_944_; lean_object* v___x_946_; uint8_t v_isShared_947_; uint8_t v_isSharedCheck_995_;
|
||||
v___x_935_ = lean_st_ref_take(v_a_929_);
|
||||
v_share_936_ = lean_ctor_get(v___x_935_, 0);
|
||||
v_maxFVar_937_ = lean_ctor_get(v___x_935_, 1);
|
||||
v_proofInstInfo_938_ = lean_ctor_get(v___x_935_, 2);
|
||||
v_inferType_939_ = lean_ctor_get(v___x_935_, 3);
|
||||
v_getLevel_940_ = lean_ctor_get(v___x_935_, 4);
|
||||
v_congrInfo_941_ = lean_ctor_get(v___x_935_, 5);
|
||||
v_defEqI_942_ = lean_ctor_get(v___x_935_, 6);
|
||||
v_extensions_943_ = lean_ctor_get(v___x_935_, 7);
|
||||
v_debug_944_ = lean_ctor_get_uint8(v___x_935_, sizeof(void*)*8);
|
||||
v_isSharedCheck_995_ = !lean_is_exclusive(v___x_935_);
|
||||
if (v_isSharedCheck_995_ == 0)
|
||||
{
|
||||
v___x_946_ = v___x_935_;
|
||||
v_isShared_947_ = v_isSharedCheck_995_;
|
||||
goto v_resetjp_945_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_extensions_943_);
|
||||
lean_inc(v_defEqI_942_);
|
||||
lean_inc(v_congrInfo_941_);
|
||||
lean_inc(v_getLevel_940_);
|
||||
lean_inc(v_inferType_939_);
|
||||
lean_inc(v_proofInstInfo_938_);
|
||||
lean_inc(v_maxFVar_937_);
|
||||
lean_inc(v_share_936_);
|
||||
lean_dec(v___x_935_);
|
||||
v___x_946_ = lean_box(0);
|
||||
v_isShared_947_ = v_isSharedCheck_995_;
|
||||
goto v_resetjp_945_;
|
||||
}
|
||||
v_resetjp_945_:
|
||||
{
|
||||
lean_object* v___x_948_; lean_object* v___x_950_;
|
||||
v___x_948_ = lean_obj_once(&l_Lean_Meta_Sym_replaceS___redArg___closed__2, &l_Lean_Meta_Sym_replaceS___redArg___closed__2_once, _init_l_Lean_Meta_Sym_replaceS___redArg___closed__2);
|
||||
if (v_isShared_947_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_946_, 0, v___x_948_);
|
||||
v___x_950_ = v___x_946_;
|
||||
goto v_reusejp_949_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_994_;
|
||||
v_reuseFailAlloc_994_ = lean_alloc_ctor(0, 8, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_994_, 0, v___x_948_);
|
||||
lean_ctor_set(v_reuseFailAlloc_994_, 1, v_maxFVar_937_);
|
||||
lean_ctor_set(v_reuseFailAlloc_994_, 2, v_proofInstInfo_938_);
|
||||
lean_ctor_set(v_reuseFailAlloc_994_, 3, v_inferType_939_);
|
||||
lean_ctor_set(v_reuseFailAlloc_994_, 4, v_getLevel_940_);
|
||||
lean_ctor_set(v_reuseFailAlloc_994_, 5, v_congrInfo_941_);
|
||||
lean_ctor_set(v_reuseFailAlloc_994_, 6, v_defEqI_942_);
|
||||
lean_ctor_set(v_reuseFailAlloc_994_, 7, v_extensions_943_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_994_, sizeof(void*)*8, v_debug_944_);
|
||||
v___x_950_ = v_reuseFailAlloc_994_;
|
||||
goto v_reusejp_949_;
|
||||
}
|
||||
v_reusejp_949_:
|
||||
{
|
||||
lean_object* v___x_951_; lean_object* v___x_952_; lean_object* v_fst_954_; lean_object* v_snd_955_; uint8_t v_debug_975_; lean_object* v___x_976_; lean_object* v___x_977_; lean_object* v___x_978_; lean_object* v_fst_979_;
|
||||
v___x_951_ = lean_st_ref_set(v_a_929_, v___x_950_);
|
||||
v___x_952_ = lean_st_ref_get(v_a_929_);
|
||||
v_debug_975_ = lean_ctor_get_uint8(v___x_952_, sizeof(void*)*8);
|
||||
lean_dec(v___x_952_);
|
||||
v___x_976_ = lean_unsigned_to_nat(0u);
|
||||
v___x_977_ = lean_box(v_debug_975_);
|
||||
lean_inc_ref(v_f_927_);
|
||||
lean_inc_ref(v_e_926_);
|
||||
v___x_978_ = lean_apply_4(v_f_927_, v_e_926_, v___x_976_, v___x_977_, v_share_936_);
|
||||
v_fst_979_ = lean_ctor_get(v___x_978_, 0);
|
||||
lean_inc(v_fst_979_);
|
||||
if (lean_obj_tag(v_fst_979_) == 1)
|
||||
{
|
||||
lean_object* v_snd_980_; lean_object* v_val_981_;
|
||||
lean_dec_ref(v_f_927_);
|
||||
lean_dec_ref(v_e_926_);
|
||||
v_snd_980_ = lean_ctor_get(v___x_978_, 1);
|
||||
lean_inc(v_snd_980_);
|
||||
lean_dec_ref(v___x_978_);
|
||||
v_val_981_ = lean_ctor_get(v_fst_979_, 0);
|
||||
lean_inc(v_val_981_);
|
||||
lean_dec_ref(v_fst_979_);
|
||||
v_fst_954_ = v_val_981_;
|
||||
v_snd_955_ = v_snd_980_;
|
||||
goto v___jp_953_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(v_fst_979_);
|
||||
switch(lean_obj_tag(v_e_926_))
|
||||
{
|
||||
case 9:
|
||||
{
|
||||
lean_object* v_snd_982_;
|
||||
lean_dec_ref(v_f_927_);
|
||||
v_snd_982_ = lean_ctor_get(v___x_978_, 1);
|
||||
lean_inc(v_snd_982_);
|
||||
lean_dec_ref(v___x_978_);
|
||||
v_fst_954_ = v_e_926_;
|
||||
v_snd_955_ = v_snd_982_;
|
||||
goto v___jp_953_;
|
||||
}
|
||||
case 2:
|
||||
{
|
||||
lean_object* v_snd_983_;
|
||||
lean_dec_ref(v_f_927_);
|
||||
v_snd_983_ = lean_ctor_get(v___x_978_, 1);
|
||||
lean_inc(v_snd_983_);
|
||||
lean_dec_ref(v___x_978_);
|
||||
v_fst_954_ = v_e_926_;
|
||||
v_snd_955_ = v_snd_983_;
|
||||
goto v___jp_953_;
|
||||
}
|
||||
case 0:
|
||||
{
|
||||
lean_object* v_snd_984_;
|
||||
lean_dec_ref(v_f_927_);
|
||||
v_snd_984_ = lean_ctor_get(v___x_978_, 1);
|
||||
lean_inc(v_snd_984_);
|
||||
lean_dec_ref(v___x_978_);
|
||||
v_fst_954_ = v_e_926_;
|
||||
v_snd_955_ = v_snd_984_;
|
||||
goto v___jp_953_;
|
||||
}
|
||||
case 1:
|
||||
{
|
||||
lean_object* v_snd_985_;
|
||||
lean_dec_ref(v_f_927_);
|
||||
v_snd_985_ = lean_ctor_get(v___x_978_, 1);
|
||||
lean_inc(v_snd_985_);
|
||||
lean_dec_ref(v___x_978_);
|
||||
v_fst_954_ = v_e_926_;
|
||||
v_snd_955_ = v_snd_985_;
|
||||
goto v___jp_953_;
|
||||
}
|
||||
case 4:
|
||||
{
|
||||
lean_object* v_snd_986_;
|
||||
lean_dec_ref(v_f_927_);
|
||||
v_snd_986_ = lean_ctor_get(v___x_978_, 1);
|
||||
lean_inc(v_snd_986_);
|
||||
lean_dec_ref(v___x_978_);
|
||||
v_fst_954_ = v_e_926_;
|
||||
v_snd_955_ = v_snd_986_;
|
||||
goto v___jp_953_;
|
||||
}
|
||||
case 3:
|
||||
{
|
||||
lean_object* v_snd_987_;
|
||||
lean_dec_ref(v_f_927_);
|
||||
v_snd_987_ = lean_ctor_get(v___x_978_, 1);
|
||||
lean_inc(v_snd_987_);
|
||||
lean_dec_ref(v___x_978_);
|
||||
v_fst_954_ = v_e_926_;
|
||||
v_snd_955_ = v_snd_987_;
|
||||
goto v___jp_953_;
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* v_snd_988_; lean_object* v___x_989_; lean_object* v___x_990_; lean_object* v_fst_991_; lean_object* v_snd_992_; lean_object* v_fst_993_;
|
||||
v_snd_988_ = lean_ctor_get(v___x_978_, 1);
|
||||
lean_inc(v_snd_988_);
|
||||
lean_dec_ref(v___x_978_);
|
||||
v___x_989_ = lean_obj_once(&l_Lean_Meta_Sym_replaceS_x27___closed__1, &l_Lean_Meta_Sym_replaceS_x27___closed__1_once, _init_l_Lean_Meta_Sym_replaceS_x27___closed__1);
|
||||
v___x_990_ = l___private_Lean_Meta_Sym_ReplaceS_0__Lean_Meta_Sym_visit(v_e_926_, v___x_976_, v_f_927_, v___x_989_, v_debug_975_, v_snd_988_);
|
||||
v_fst_991_ = lean_ctor_get(v___x_990_, 0);
|
||||
lean_inc(v_fst_991_);
|
||||
v_snd_992_ = lean_ctor_get(v___x_990_, 1);
|
||||
lean_inc(v_snd_992_);
|
||||
lean_dec_ref(v___x_990_);
|
||||
v_fst_993_ = lean_ctor_get(v_fst_991_, 0);
|
||||
lean_inc(v_fst_993_);
|
||||
lean_dec(v_fst_991_);
|
||||
v_fst_954_ = v_fst_993_;
|
||||
v_snd_955_ = v_snd_992_;
|
||||
goto v___jp_953_;
|
||||
}
|
||||
}
|
||||
}
|
||||
v___jp_953_:
|
||||
{
|
||||
lean_object* v___x_956_; lean_object* v_maxFVar_957_; lean_object* v_proofInstInfo_958_; lean_object* v_inferType_959_; lean_object* v_getLevel_960_; lean_object* v_congrInfo_961_; lean_object* v_defEqI_962_; lean_object* v_extensions_963_; uint8_t v_debug_964_; lean_object* v___x_966_; uint8_t v_isShared_967_; uint8_t v_isSharedCheck_973_;
|
||||
v___x_956_ = lean_st_ref_take(v_a_929_);
|
||||
v_maxFVar_957_ = lean_ctor_get(v___x_956_, 1);
|
||||
v_proofInstInfo_958_ = lean_ctor_get(v___x_956_, 2);
|
||||
v_inferType_959_ = lean_ctor_get(v___x_956_, 3);
|
||||
v_getLevel_960_ = lean_ctor_get(v___x_956_, 4);
|
||||
v_congrInfo_961_ = lean_ctor_get(v___x_956_, 5);
|
||||
v_defEqI_962_ = lean_ctor_get(v___x_956_, 6);
|
||||
v_extensions_963_ = lean_ctor_get(v___x_956_, 7);
|
||||
v_debug_964_ = lean_ctor_get_uint8(v___x_956_, sizeof(void*)*8);
|
||||
v_isSharedCheck_973_ = !lean_is_exclusive(v___x_956_);
|
||||
if (v_isSharedCheck_973_ == 0)
|
||||
{
|
||||
lean_object* v_unused_974_;
|
||||
v_unused_974_ = lean_ctor_get(v___x_956_, 0);
|
||||
lean_dec(v_unused_974_);
|
||||
v___x_966_ = v___x_956_;
|
||||
v_isShared_967_ = v_isSharedCheck_973_;
|
||||
goto v_resetjp_965_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_extensions_963_);
|
||||
lean_inc(v_defEqI_962_);
|
||||
lean_inc(v_congrInfo_961_);
|
||||
lean_inc(v_getLevel_960_);
|
||||
lean_inc(v_inferType_959_);
|
||||
lean_inc(v_proofInstInfo_958_);
|
||||
lean_inc(v_maxFVar_957_);
|
||||
lean_dec(v___x_956_);
|
||||
v___x_966_ = lean_box(0);
|
||||
v_isShared_967_ = v_isSharedCheck_973_;
|
||||
goto v_resetjp_965_;
|
||||
}
|
||||
v_resetjp_965_:
|
||||
{
|
||||
lean_object* v___x_969_;
|
||||
if (v_isShared_967_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_966_, 0, v_snd_955_);
|
||||
v___x_969_ = v___x_966_;
|
||||
goto v_reusejp_968_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_972_;
|
||||
v_reuseFailAlloc_972_ = lean_alloc_ctor(0, 8, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_972_, 0, v_snd_955_);
|
||||
lean_ctor_set(v_reuseFailAlloc_972_, 1, v_maxFVar_957_);
|
||||
lean_ctor_set(v_reuseFailAlloc_972_, 2, v_proofInstInfo_958_);
|
||||
lean_ctor_set(v_reuseFailAlloc_972_, 3, v_inferType_959_);
|
||||
lean_ctor_set(v_reuseFailAlloc_972_, 4, v_getLevel_960_);
|
||||
lean_ctor_set(v_reuseFailAlloc_972_, 5, v_congrInfo_961_);
|
||||
lean_ctor_set(v_reuseFailAlloc_972_, 6, v_defEqI_962_);
|
||||
lean_ctor_set(v_reuseFailAlloc_972_, 7, v_extensions_963_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_972_, sizeof(void*)*8, v_debug_964_);
|
||||
v___x_969_ = v_reuseFailAlloc_972_;
|
||||
goto v_reusejp_968_;
|
||||
}
|
||||
v_reusejp_968_:
|
||||
{
|
||||
lean_object* v___x_970_; lean_object* v___x_971_;
|
||||
v___x_970_ = lean_st_ref_set(v_a_929_, v___x_969_);
|
||||
v___x_971_ = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(v___x_971_, 0, v_fst_954_);
|
||||
return v___x_971_;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_replaceS___boxed(lean_object* v_e_996_, lean_object* v_f_997_, lean_object* v_a_998_, lean_object* v_a_999_, lean_object* v_a_1000_, lean_object* v_a_1001_, lean_object* v_a_1002_, lean_object* v_a_1003_, lean_object* v_a_1004_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_1005_;
|
||||
v_res_1005_ = l_Lean_Meta_Sym_replaceS(v_e_996_, v_f_997_, v_a_998_, v_a_999_, v_a_1000_, v_a_1001_, v_a_1002_, v_a_1003_);
|
||||
lean_dec(v_a_1003_);
|
||||
lean_dec_ref(v_a_1002_);
|
||||
lean_dec(v_a_1001_);
|
||||
lean_dec_ref(v_a_1000_);
|
||||
lean_dec(v_a_999_);
|
||||
lean_dec_ref(v_a_998_);
|
||||
lean_dec(v_a_997_);
|
||||
lean_dec_ref(v_a_996_);
|
||||
lean_dec(v_a_995_);
|
||||
lean_dec_ref(v_a_994_);
|
||||
return v_res_1001_;
|
||||
return v_res_1005_;
|
||||
}
|
||||
}
|
||||
lean_object* runtime_initialize_Lean_Meta_Sym_AlphaShareBuilder(uint8_t builtin);
|
||||
|
|
|
|||
8128
stage0/stdlib/Lean/Meta/Sym/Simp/App.c
generated
8128
stage0/stdlib/Lean/Meta/Sym/Simp/App.c
generated
File diff suppressed because it is too large
Load diff
607
stage0/stdlib/Lean/Meta/Sym/Simp/CongrInfo.c
generated
607
stage0/stdlib/Lean/Meta/Sym/Simp/CongrInfo.c
generated
|
|
@ -1887,12 +1887,12 @@ return v_res_495_;
|
|||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2___redArg___boxed(lean_object* v_x_496_, lean_object* v_x_497_, lean_object* v_x_498_, lean_object* v_x_499_, lean_object* v_x_500_){
|
||||
_start:
|
||||
{
|
||||
size_t v_x_2476__boxed_501_; size_t v_x_2477__boxed_502_; lean_object* v_res_503_;
|
||||
v_x_2476__boxed_501_ = lean_unbox_usize(v_x_497_);
|
||||
size_t v_x_2499__boxed_501_; size_t v_x_2500__boxed_502_; lean_object* v_res_503_;
|
||||
v_x_2499__boxed_501_ = lean_unbox_usize(v_x_497_);
|
||||
lean_dec(v_x_497_);
|
||||
v_x_2477__boxed_502_ = lean_unbox_usize(v_x_498_);
|
||||
v_x_2500__boxed_502_ = lean_unbox_usize(v_x_498_);
|
||||
lean_dec(v_x_498_);
|
||||
v_res_503_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2___redArg(v_x_496_, v_x_2476__boxed_501_, v_x_2477__boxed_502_, v_x_499_, v_x_500_);
|
||||
v_res_503_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2___redArg(v_x_496_, v_x_2499__boxed_501_, v_x_2500__boxed_502_, v_x_499_, v_x_500_);
|
||||
return v_res_503_;
|
||||
}
|
||||
}
|
||||
|
|
@ -2076,10 +2076,10 @@ return v___x_558_;
|
|||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0___redArg___boxed(lean_object* v_x_559_, lean_object* v_x_560_, lean_object* v_x_561_){
|
||||
_start:
|
||||
{
|
||||
size_t v_x_2676__boxed_562_; lean_object* v_res_563_;
|
||||
v_x_2676__boxed_562_ = lean_unbox_usize(v_x_560_);
|
||||
size_t v_x_2699__boxed_562_; lean_object* v_res_563_;
|
||||
v_x_2699__boxed_562_ = lean_unbox_usize(v_x_560_);
|
||||
lean_dec(v_x_560_);
|
||||
v_res_563_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0___redArg(v_x_559_, v_x_2676__boxed_562_, v_x_561_);
|
||||
v_res_563_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0___redArg(v_x_559_, v_x_2699__boxed_562_, v_x_561_);
|
||||
lean_dec_ref(v_x_561_);
|
||||
return v_res_563_;
|
||||
}
|
||||
|
|
@ -2163,13 +2163,13 @@ lean_inc_ref(v_f_572_);
|
|||
v___x_590_ = l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_mkCongrInfo___redArg(v_f_572_, v_a_574_, v_a_575_, v_a_576_, v_a_577_);
|
||||
if (lean_obj_tag(v___x_590_) == 0)
|
||||
{
|
||||
lean_object* v_a_591_; lean_object* v___x_593_; uint8_t v_isShared_594_; uint8_t v_isSharedCheck_616_;
|
||||
lean_object* v_a_591_; lean_object* v___x_593_; uint8_t v_isShared_594_; uint8_t v_isSharedCheck_617_;
|
||||
v_a_591_ = lean_ctor_get(v___x_590_, 0);
|
||||
v_isSharedCheck_616_ = !lean_is_exclusive(v___x_590_);
|
||||
if (v_isSharedCheck_616_ == 0)
|
||||
v_isSharedCheck_617_ = !lean_is_exclusive(v___x_590_);
|
||||
if (v_isSharedCheck_617_ == 0)
|
||||
{
|
||||
v___x_593_ = v___x_590_;
|
||||
v_isShared_594_ = v_isSharedCheck_616_;
|
||||
v_isShared_594_ = v_isSharedCheck_617_;
|
||||
goto v_resetjp_592_;
|
||||
}
|
||||
else
|
||||
|
|
@ -2177,12 +2177,12 @@ else
|
|||
lean_inc(v_a_591_);
|
||||
lean_dec(v___x_590_);
|
||||
v___x_593_ = lean_box(0);
|
||||
v_isShared_594_ = v_isSharedCheck_616_;
|
||||
v_isShared_594_ = v_isSharedCheck_617_;
|
||||
goto v_resetjp_592_;
|
||||
}
|
||||
v_resetjp_592_:
|
||||
{
|
||||
lean_object* v___x_595_; lean_object* v_share_596_; lean_object* v_maxFVar_597_; lean_object* v_proofInstInfo_598_; lean_object* v_inferType_599_; lean_object* v_getLevel_600_; lean_object* v_congrInfo_601_; lean_object* v_defEqI_602_; uint8_t v_debug_603_; lean_object* v___x_605_; uint8_t v_isShared_606_; uint8_t v_isSharedCheck_615_;
|
||||
lean_object* v___x_595_; lean_object* v_share_596_; lean_object* v_maxFVar_597_; lean_object* v_proofInstInfo_598_; lean_object* v_inferType_599_; lean_object* v_getLevel_600_; lean_object* v_congrInfo_601_; lean_object* v_defEqI_602_; lean_object* v_extensions_603_; uint8_t v_debug_604_; lean_object* v___x_606_; uint8_t v_isShared_607_; uint8_t v_isSharedCheck_616_;
|
||||
v___x_595_ = lean_st_ref_take(v_a_573_);
|
||||
v_share_596_ = lean_ctor_get(v___x_595_, 0);
|
||||
v_maxFVar_597_ = lean_ctor_get(v___x_595_, 1);
|
||||
|
|
@ -2191,16 +2191,18 @@ v_inferType_599_ = lean_ctor_get(v___x_595_, 3);
|
|||
v_getLevel_600_ = lean_ctor_get(v___x_595_, 4);
|
||||
v_congrInfo_601_ = lean_ctor_get(v___x_595_, 5);
|
||||
v_defEqI_602_ = lean_ctor_get(v___x_595_, 6);
|
||||
v_debug_603_ = lean_ctor_get_uint8(v___x_595_, sizeof(void*)*7);
|
||||
v_isSharedCheck_615_ = !lean_is_exclusive(v___x_595_);
|
||||
if (v_isSharedCheck_615_ == 0)
|
||||
v_extensions_603_ = lean_ctor_get(v___x_595_, 7);
|
||||
v_debug_604_ = lean_ctor_get_uint8(v___x_595_, sizeof(void*)*8);
|
||||
v_isSharedCheck_616_ = !lean_is_exclusive(v___x_595_);
|
||||
if (v_isSharedCheck_616_ == 0)
|
||||
{
|
||||
v___x_605_ = v___x_595_;
|
||||
v_isShared_606_ = v_isSharedCheck_615_;
|
||||
goto v_resetjp_604_;
|
||||
v___x_606_ = v___x_595_;
|
||||
v_isShared_607_ = v_isSharedCheck_616_;
|
||||
goto v_resetjp_605_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_extensions_603_);
|
||||
lean_inc(v_defEqI_602_);
|
||||
lean_inc(v_congrInfo_601_);
|
||||
lean_inc(v_getLevel_600_);
|
||||
|
|
@ -2209,56 +2211,57 @@ lean_inc(v_proofInstInfo_598_);
|
|||
lean_inc(v_maxFVar_597_);
|
||||
lean_inc(v_share_596_);
|
||||
lean_dec(v___x_595_);
|
||||
v___x_605_ = lean_box(0);
|
||||
v_isShared_606_ = v_isSharedCheck_615_;
|
||||
goto v_resetjp_604_;
|
||||
v___x_606_ = lean_box(0);
|
||||
v_isShared_607_ = v_isSharedCheck_616_;
|
||||
goto v_resetjp_605_;
|
||||
}
|
||||
v_resetjp_604_:
|
||||
v_resetjp_605_:
|
||||
{
|
||||
lean_object* v___x_607_; lean_object* v___x_609_;
|
||||
lean_object* v___x_608_; lean_object* v___x_610_;
|
||||
lean_inc(v_a_591_);
|
||||
v___x_607_ = l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1___redArg(v_congrInfo_601_, v_f_572_, v_a_591_);
|
||||
if (v_isShared_606_ == 0)
|
||||
v___x_608_ = l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1___redArg(v_congrInfo_601_, v_f_572_, v_a_591_);
|
||||
if (v_isShared_607_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_605_, 5, v___x_607_);
|
||||
v___x_609_ = v___x_605_;
|
||||
goto v_reusejp_608_;
|
||||
lean_ctor_set(v___x_606_, 5, v___x_608_);
|
||||
v___x_610_ = v___x_606_;
|
||||
goto v_reusejp_609_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_615_;
|
||||
v_reuseFailAlloc_615_ = lean_alloc_ctor(0, 8, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_615_, 0, v_share_596_);
|
||||
lean_ctor_set(v_reuseFailAlloc_615_, 1, v_maxFVar_597_);
|
||||
lean_ctor_set(v_reuseFailAlloc_615_, 2, v_proofInstInfo_598_);
|
||||
lean_ctor_set(v_reuseFailAlloc_615_, 3, v_inferType_599_);
|
||||
lean_ctor_set(v_reuseFailAlloc_615_, 4, v_getLevel_600_);
|
||||
lean_ctor_set(v_reuseFailAlloc_615_, 5, v___x_608_);
|
||||
lean_ctor_set(v_reuseFailAlloc_615_, 6, v_defEqI_602_);
|
||||
lean_ctor_set(v_reuseFailAlloc_615_, 7, v_extensions_603_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_615_, sizeof(void*)*8, v_debug_604_);
|
||||
v___x_610_ = v_reuseFailAlloc_615_;
|
||||
goto v_reusejp_609_;
|
||||
}
|
||||
v_reusejp_609_:
|
||||
{
|
||||
lean_object* v___x_611_; lean_object* v___x_613_;
|
||||
v___x_611_ = lean_st_ref_set(v_a_573_, v___x_610_);
|
||||
if (v_isShared_594_ == 0)
|
||||
{
|
||||
v___x_613_ = v___x_593_;
|
||||
goto v_reusejp_612_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_614_;
|
||||
v_reuseFailAlloc_614_ = lean_alloc_ctor(0, 7, 1);
|
||||
lean_ctor_set(v_reuseFailAlloc_614_, 0, v_share_596_);
|
||||
lean_ctor_set(v_reuseFailAlloc_614_, 1, v_maxFVar_597_);
|
||||
lean_ctor_set(v_reuseFailAlloc_614_, 2, v_proofInstInfo_598_);
|
||||
lean_ctor_set(v_reuseFailAlloc_614_, 3, v_inferType_599_);
|
||||
lean_ctor_set(v_reuseFailAlloc_614_, 4, v_getLevel_600_);
|
||||
lean_ctor_set(v_reuseFailAlloc_614_, 5, v___x_607_);
|
||||
lean_ctor_set(v_reuseFailAlloc_614_, 6, v_defEqI_602_);
|
||||
lean_ctor_set_uint8(v_reuseFailAlloc_614_, sizeof(void*)*7, v_debug_603_);
|
||||
v___x_609_ = v_reuseFailAlloc_614_;
|
||||
goto v_reusejp_608_;
|
||||
v_reuseFailAlloc_614_ = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(v_reuseFailAlloc_614_, 0, v_a_591_);
|
||||
v___x_613_ = v_reuseFailAlloc_614_;
|
||||
goto v_reusejp_612_;
|
||||
}
|
||||
v_reusejp_608_:
|
||||
v_reusejp_612_:
|
||||
{
|
||||
lean_object* v___x_610_; lean_object* v___x_612_;
|
||||
v___x_610_ = lean_st_ref_set(v_a_573_, v___x_609_);
|
||||
if (v_isShared_594_ == 0)
|
||||
{
|
||||
v___x_612_ = v___x_593_;
|
||||
goto v_reusejp_611_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_613_;
|
||||
v_reuseFailAlloc_613_ = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(v_reuseFailAlloc_613_, 0, v_a_591_);
|
||||
v___x_612_ = v_reuseFailAlloc_613_;
|
||||
goto v_reusejp_611_;
|
||||
}
|
||||
v_reusejp_611_:
|
||||
{
|
||||
return v___x_612_;
|
||||
return v___x_613_;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -2272,235 +2275,235 @@ return v___x_590_;
|
|||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getCongrInfo___redArg___boxed(lean_object* v_f_617_, lean_object* v_a_618_, lean_object* v_a_619_, lean_object* v_a_620_, lean_object* v_a_621_, lean_object* v_a_622_, lean_object* v_a_623_){
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getCongrInfo___redArg___boxed(lean_object* v_f_618_, lean_object* v_a_619_, lean_object* v_a_620_, lean_object* v_a_621_, lean_object* v_a_622_, lean_object* v_a_623_, lean_object* v_a_624_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_624_;
|
||||
v_res_624_ = l_Lean_Meta_Sym_getCongrInfo___redArg(v_f_617_, v_a_618_, v_a_619_, v_a_620_, v_a_621_, v_a_622_);
|
||||
lean_dec(v_a_622_);
|
||||
lean_dec_ref(v_a_621_);
|
||||
lean_dec(v_a_620_);
|
||||
lean_dec_ref(v_a_619_);
|
||||
lean_dec(v_a_618_);
|
||||
return v_res_624_;
|
||||
lean_object* v_res_625_;
|
||||
v_res_625_ = l_Lean_Meta_Sym_getCongrInfo___redArg(v_f_618_, v_a_619_, v_a_620_, v_a_621_, v_a_622_, v_a_623_);
|
||||
lean_dec(v_a_623_);
|
||||
lean_dec_ref(v_a_622_);
|
||||
lean_dec(v_a_621_);
|
||||
lean_dec_ref(v_a_620_);
|
||||
lean_dec(v_a_619_);
|
||||
return v_res_625_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getCongrInfo(lean_object* v_f_625_, lean_object* v_a_626_, lean_object* v_a_627_, lean_object* v_a_628_, lean_object* v_a_629_, lean_object* v_a_630_, lean_object* v_a_631_){
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getCongrInfo(lean_object* v_f_626_, lean_object* v_a_627_, lean_object* v_a_628_, lean_object* v_a_629_, lean_object* v_a_630_, lean_object* v_a_631_, lean_object* v_a_632_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_633_;
|
||||
v___x_633_ = l_Lean_Meta_Sym_getCongrInfo___redArg(v_f_625_, v_a_627_, v_a_628_, v_a_629_, v_a_630_, v_a_631_);
|
||||
return v___x_633_;
|
||||
lean_object* v___x_634_;
|
||||
v___x_634_ = l_Lean_Meta_Sym_getCongrInfo___redArg(v_f_626_, v_a_628_, v_a_629_, v_a_630_, v_a_631_, v_a_632_);
|
||||
return v___x_634_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getCongrInfo___boxed(lean_object* v_f_634_, lean_object* v_a_635_, lean_object* v_a_636_, lean_object* v_a_637_, lean_object* v_a_638_, lean_object* v_a_639_, lean_object* v_a_640_, lean_object* v_a_641_){
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_Sym_getCongrInfo___boxed(lean_object* v_f_635_, lean_object* v_a_636_, lean_object* v_a_637_, lean_object* v_a_638_, lean_object* v_a_639_, lean_object* v_a_640_, lean_object* v_a_641_, lean_object* v_a_642_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_642_;
|
||||
v_res_642_ = l_Lean_Meta_Sym_getCongrInfo(v_f_634_, v_a_635_, v_a_636_, v_a_637_, v_a_638_, v_a_639_, v_a_640_);
|
||||
lean_dec(v_a_640_);
|
||||
lean_dec_ref(v_a_639_);
|
||||
lean_dec(v_a_638_);
|
||||
lean_dec_ref(v_a_637_);
|
||||
lean_dec(v_a_636_);
|
||||
lean_dec_ref(v_a_635_);
|
||||
return v_res_642_;
|
||||
lean_object* v_res_643_;
|
||||
v_res_643_ = l_Lean_Meta_Sym_getCongrInfo(v_f_635_, v_a_636_, v_a_637_, v_a_638_, v_a_639_, v_a_640_, v_a_641_);
|
||||
lean_dec(v_a_641_);
|
||||
lean_dec_ref(v_a_640_);
|
||||
lean_dec(v_a_639_);
|
||||
lean_dec_ref(v_a_638_);
|
||||
lean_dec(v_a_637_);
|
||||
lean_dec_ref(v_a_636_);
|
||||
return v_res_643_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0(lean_object* v_00_u03b2_643_, lean_object* v_x_644_, lean_object* v_x_645_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0(lean_object* v_00_u03b2_644_, lean_object* v_x_645_, lean_object* v_x_646_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_646_;
|
||||
v___x_646_ = l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0___redArg(v_x_644_, v_x_645_);
|
||||
return v___x_646_;
|
||||
lean_object* v___x_647_;
|
||||
v___x_647_ = l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0___redArg(v_x_645_, v_x_646_);
|
||||
return v___x_647_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0___boxed(lean_object* v_00_u03b2_647_, lean_object* v_x_648_, lean_object* v_x_649_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0___boxed(lean_object* v_00_u03b2_648_, lean_object* v_x_649_, lean_object* v_x_650_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_650_;
|
||||
v_res_650_ = l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0(v_00_u03b2_647_, v_x_648_, v_x_649_);
|
||||
lean_dec_ref(v_x_649_);
|
||||
return v_res_650_;
|
||||
lean_object* v_res_651_;
|
||||
v_res_651_ = l_Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0(v_00_u03b2_648_, v_x_649_, v_x_650_);
|
||||
lean_dec_ref(v_x_650_);
|
||||
return v_res_651_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1(lean_object* v_00_u03b2_651_, lean_object* v_x_652_, lean_object* v_x_653_, lean_object* v_x_654_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1(lean_object* v_00_u03b2_652_, lean_object* v_x_653_, lean_object* v_x_654_, lean_object* v_x_655_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_655_;
|
||||
v___x_655_ = l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1___redArg(v_x_652_, v_x_653_, v_x_654_);
|
||||
return v___x_655_;
|
||||
lean_object* v___x_656_;
|
||||
v___x_656_ = l_Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1___redArg(v_x_653_, v_x_654_, v_x_655_);
|
||||
return v___x_656_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0(lean_object* v_00_u03b2_656_, lean_object* v_x_657_, size_t v_x_658_, lean_object* v_x_659_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0(lean_object* v_00_u03b2_657_, lean_object* v_x_658_, size_t v_x_659_, lean_object* v_x_660_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_660_;
|
||||
v___x_660_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0___redArg(v_x_657_, v_x_658_, v_x_659_);
|
||||
return v___x_660_;
|
||||
lean_object* v___x_661_;
|
||||
v___x_661_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0___redArg(v_x_658_, v_x_659_, v_x_660_);
|
||||
return v___x_661_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0___boxed(lean_object* v_00_u03b2_661_, lean_object* v_x_662_, lean_object* v_x_663_, lean_object* v_x_664_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0___boxed(lean_object* v_00_u03b2_662_, lean_object* v_x_663_, lean_object* v_x_664_, lean_object* v_x_665_){
|
||||
_start:
|
||||
{
|
||||
size_t v_x_2832__boxed_665_; lean_object* v_res_666_;
|
||||
v_x_2832__boxed_665_ = lean_unbox_usize(v_x_663_);
|
||||
lean_dec(v_x_663_);
|
||||
v_res_666_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0(v_00_u03b2_661_, v_x_662_, v_x_2832__boxed_665_, v_x_664_);
|
||||
lean_dec_ref(v_x_664_);
|
||||
return v_res_666_;
|
||||
size_t v_x_2855__boxed_666_; lean_object* v_res_667_;
|
||||
v_x_2855__boxed_666_ = lean_unbox_usize(v_x_664_);
|
||||
lean_dec(v_x_664_);
|
||||
v_res_667_ = l_Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0(v_00_u03b2_662_, v_x_663_, v_x_2855__boxed_666_, v_x_665_);
|
||||
lean_dec_ref(v_x_665_);
|
||||
return v_res_667_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2(lean_object* v_00_u03b2_667_, lean_object* v_x_668_, size_t v_x_669_, size_t v_x_670_, lean_object* v_x_671_, lean_object* v_x_672_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2(lean_object* v_00_u03b2_668_, lean_object* v_x_669_, size_t v_x_670_, size_t v_x_671_, lean_object* v_x_672_, lean_object* v_x_673_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_673_;
|
||||
v___x_673_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2___redArg(v_x_668_, v_x_669_, v_x_670_, v_x_671_, v_x_672_);
|
||||
return v___x_673_;
|
||||
lean_object* v___x_674_;
|
||||
v___x_674_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2___redArg(v_x_669_, v_x_670_, v_x_671_, v_x_672_, v_x_673_);
|
||||
return v___x_674_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2___boxed(lean_object* v_00_u03b2_674_, lean_object* v_x_675_, lean_object* v_x_676_, lean_object* v_x_677_, lean_object* v_x_678_, lean_object* v_x_679_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2___boxed(lean_object* v_00_u03b2_675_, lean_object* v_x_676_, lean_object* v_x_677_, lean_object* v_x_678_, lean_object* v_x_679_, lean_object* v_x_680_){
|
||||
_start:
|
||||
{
|
||||
size_t v_x_2843__boxed_680_; size_t v_x_2844__boxed_681_; lean_object* v_res_682_;
|
||||
v_x_2843__boxed_680_ = lean_unbox_usize(v_x_676_);
|
||||
lean_dec(v_x_676_);
|
||||
v_x_2844__boxed_681_ = lean_unbox_usize(v_x_677_);
|
||||
size_t v_x_2866__boxed_681_; size_t v_x_2867__boxed_682_; lean_object* v_res_683_;
|
||||
v_x_2866__boxed_681_ = lean_unbox_usize(v_x_677_);
|
||||
lean_dec(v_x_677_);
|
||||
v_res_682_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2(v_00_u03b2_674_, v_x_675_, v_x_2843__boxed_680_, v_x_2844__boxed_681_, v_x_678_, v_x_679_);
|
||||
return v_res_682_;
|
||||
v_x_2867__boxed_682_ = lean_unbox_usize(v_x_678_);
|
||||
lean_dec(v_x_678_);
|
||||
v_res_683_ = l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2(v_00_u03b2_675_, v_x_676_, v_x_2866__boxed_681_, v_x_2867__boxed_682_, v_x_679_, v_x_680_);
|
||||
return v_res_683_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0_spec__1(lean_object* v_00_u03b2_683_, lean_object* v_keys_684_, lean_object* v_vals_685_, lean_object* v_heq_686_, lean_object* v_i_687_, lean_object* v_k_688_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0_spec__1(lean_object* v_00_u03b2_684_, lean_object* v_keys_685_, lean_object* v_vals_686_, lean_object* v_heq_687_, lean_object* v_i_688_, lean_object* v_k_689_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_689_;
|
||||
v___x_689_ = l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0_spec__1___redArg(v_keys_684_, v_vals_685_, v_i_687_, v_k_688_);
|
||||
return v___x_689_;
|
||||
lean_object* v___x_690_;
|
||||
v___x_690_ = l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0_spec__1___redArg(v_keys_685_, v_vals_686_, v_i_688_, v_k_689_);
|
||||
return v___x_690_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0_spec__1___boxed(lean_object* v_00_u03b2_690_, lean_object* v_keys_691_, lean_object* v_vals_692_, lean_object* v_heq_693_, lean_object* v_i_694_, lean_object* v_k_695_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0_spec__1___boxed(lean_object* v_00_u03b2_691_, lean_object* v_keys_692_, lean_object* v_vals_693_, lean_object* v_heq_694_, lean_object* v_i_695_, lean_object* v_k_696_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v_res_696_;
|
||||
v_res_696_ = l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0_spec__1(v_00_u03b2_690_, v_keys_691_, v_vals_692_, v_heq_693_, v_i_694_, v_k_695_);
|
||||
lean_dec_ref(v_k_695_);
|
||||
lean_dec_ref(v_vals_692_);
|
||||
lean_dec_ref(v_keys_691_);
|
||||
return v_res_696_;
|
||||
lean_object* v_res_697_;
|
||||
v_res_697_ = l_Lean_PersistentHashMap_findAtAux___at___00Lean_PersistentHashMap_findAux___at___00Lean_PersistentHashMap_find_x3f___at___00Lean_Meta_Sym_getCongrInfo_spec__0_spec__0_spec__1(v_00_u03b2_691_, v_keys_692_, v_vals_693_, v_heq_694_, v_i_695_, v_k_696_);
|
||||
lean_dec_ref(v_k_696_);
|
||||
lean_dec_ref(v_vals_693_);
|
||||
lean_dec_ref(v_keys_692_);
|
||||
return v_res_697_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__4(lean_object* v_00_u03b2_697_, lean_object* v_n_698_, lean_object* v_k_699_, lean_object* v_v_700_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__4(lean_object* v_00_u03b2_698_, lean_object* v_n_699_, lean_object* v_k_700_, lean_object* v_v_701_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_701_;
|
||||
v___x_701_ = l_Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__4___redArg(v_n_698_, v_k_699_, v_v_700_);
|
||||
return v___x_701_;
|
||||
lean_object* v___x_702_;
|
||||
v___x_702_ = l_Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__4___redArg(v_n_699_, v_k_700_, v_v_701_);
|
||||
return v___x_702_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__5(lean_object* v_00_u03b2_702_, size_t v_depth_703_, lean_object* v_keys_704_, lean_object* v_vals_705_, lean_object* v_heq_706_, lean_object* v_i_707_, lean_object* v_entries_708_){
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__5(lean_object* v_00_u03b2_703_, size_t v_depth_704_, lean_object* v_keys_705_, lean_object* v_vals_706_, lean_object* v_heq_707_, lean_object* v_i_708_, lean_object* v_entries_709_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_709_;
|
||||
v___x_709_ = l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__5___redArg(v_depth_703_, v_keys_704_, v_vals_705_, v_i_707_, v_entries_708_);
|
||||
return v___x_709_;
|
||||
lean_object* v___x_710_;
|
||||
v___x_710_ = l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__5___redArg(v_depth_704_, v_keys_705_, v_vals_706_, v_i_708_, v_entries_709_);
|
||||
return v___x_710_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__5___boxed(lean_object* v_00_u03b2_710_, lean_object* v_depth_711_, lean_object* v_keys_712_, lean_object* v_vals_713_, lean_object* v_heq_714_, lean_object* v_i_715_, lean_object* v_entries_716_){
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__5___boxed(lean_object* v_00_u03b2_711_, lean_object* v_depth_712_, lean_object* v_keys_713_, lean_object* v_vals_714_, lean_object* v_heq_715_, lean_object* v_i_716_, lean_object* v_entries_717_){
|
||||
_start:
|
||||
{
|
||||
size_t v_depth_boxed_717_; lean_object* v_res_718_;
|
||||
v_depth_boxed_717_ = lean_unbox_usize(v_depth_711_);
|
||||
lean_dec(v_depth_711_);
|
||||
v_res_718_ = l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__5(v_00_u03b2_710_, v_depth_boxed_717_, v_keys_712_, v_vals_713_, v_heq_714_, v_i_715_, v_entries_716_);
|
||||
lean_dec_ref(v_vals_713_);
|
||||
lean_dec_ref(v_keys_712_);
|
||||
return v_res_718_;
|
||||
size_t v_depth_boxed_718_; lean_object* v_res_719_;
|
||||
v_depth_boxed_718_ = lean_unbox_usize(v_depth_712_);
|
||||
lean_dec(v_depth_712_);
|
||||
v_res_719_ = l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__5(v_00_u03b2_711_, v_depth_boxed_718_, v_keys_713_, v_vals_714_, v_heq_715_, v_i_716_, v_entries_717_);
|
||||
lean_dec_ref(v_vals_714_);
|
||||
lean_dec_ref(v_keys_713_);
|
||||
return v_res_719_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at___00Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__4_spec__5(lean_object* v_00_u03b2_719_, lean_object* v_x_720_, lean_object* v_x_721_, lean_object* v_x_722_, lean_object* v_x_723_){
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at___00Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__4_spec__5(lean_object* v_00_u03b2_720_, lean_object* v_x_721_, lean_object* v_x_722_, lean_object* v_x_723_, lean_object* v_x_724_){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_724_;
|
||||
v___x_724_ = l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at___00Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__4_spec__5___redArg(v_x_720_, v_x_721_, v_x_722_, v_x_723_);
|
||||
return v___x_724_;
|
||||
lean_object* v___x_725_;
|
||||
v___x_725_ = l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at___00Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_Meta_Sym_getCongrInfo_spec__1_spec__2_spec__4_spec__5___redArg(v_x_721_, v_x_722_, v_x_723_, v_x_724_);
|
||||
return v___x_725_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_List_mapTR_loop___at___00__private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData_spec__0(lean_object* v_a_727_, lean_object* v_a_728_){
|
||||
LEAN_EXPORT lean_object* l_List_mapTR_loop___at___00__private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData_spec__0(lean_object* v_a_728_, lean_object* v_a_729_){
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(v_a_727_) == 0)
|
||||
if (lean_obj_tag(v_a_728_) == 0)
|
||||
{
|
||||
lean_object* v___x_729_;
|
||||
v___x_729_ = l_List_reverse___redArg(v_a_728_);
|
||||
return v___x_729_;
|
||||
lean_object* v___x_730_;
|
||||
v___x_730_ = l_List_reverse___redArg(v_a_729_);
|
||||
return v___x_730_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_head_730_; lean_object* v_tail_731_; lean_object* v___x_733_; uint8_t v_isShared_734_; uint8_t v_isSharedCheck_746_;
|
||||
v_head_730_ = lean_ctor_get(v_a_727_, 0);
|
||||
v_tail_731_ = lean_ctor_get(v_a_727_, 1);
|
||||
v_isSharedCheck_746_ = !lean_is_exclusive(v_a_727_);
|
||||
if (v_isSharedCheck_746_ == 0)
|
||||
lean_object* v_head_731_; lean_object* v_tail_732_; lean_object* v___x_734_; uint8_t v_isShared_735_; uint8_t v_isSharedCheck_747_;
|
||||
v_head_731_ = lean_ctor_get(v_a_728_, 0);
|
||||
v_tail_732_ = lean_ctor_get(v_a_728_, 1);
|
||||
v_isSharedCheck_747_ = !lean_is_exclusive(v_a_728_);
|
||||
if (v_isSharedCheck_747_ == 0)
|
||||
{
|
||||
v___x_733_ = v_a_727_;
|
||||
v_isShared_734_ = v_isSharedCheck_746_;
|
||||
goto v_resetjp_732_;
|
||||
v___x_734_ = v_a_728_;
|
||||
v_isShared_735_ = v_isSharedCheck_747_;
|
||||
goto v_resetjp_733_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_tail_731_);
|
||||
lean_inc(v_head_730_);
|
||||
lean_dec(v_a_727_);
|
||||
v___x_733_ = lean_box(0);
|
||||
v_isShared_734_ = v_isSharedCheck_746_;
|
||||
goto v_resetjp_732_;
|
||||
lean_inc(v_tail_732_);
|
||||
lean_inc(v_head_731_);
|
||||
lean_dec(v_a_728_);
|
||||
v___x_734_ = lean_box(0);
|
||||
v_isShared_735_ = v_isSharedCheck_747_;
|
||||
goto v_resetjp_733_;
|
||||
}
|
||||
v_resetjp_732_:
|
||||
v_resetjp_733_:
|
||||
{
|
||||
lean_object* v___y_736_; uint8_t v___x_743_;
|
||||
v___x_743_ = lean_unbox(v_head_730_);
|
||||
lean_dec(v_head_730_);
|
||||
if (v___x_743_ == 0)
|
||||
{
|
||||
lean_object* v___x_744_;
|
||||
v___x_744_ = ((lean_object*)(l_List_mapTR_loop___at___00__private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData_spec__0___closed__0));
|
||||
v___y_736_ = v___x_744_;
|
||||
goto v___jp_735_;
|
||||
}
|
||||
else
|
||||
lean_object* v___y_737_; uint8_t v___x_744_;
|
||||
v___x_744_ = lean_unbox(v_head_731_);
|
||||
lean_dec(v_head_731_);
|
||||
if (v___x_744_ == 0)
|
||||
{
|
||||
lean_object* v___x_745_;
|
||||
v___x_745_ = ((lean_object*)(l_List_mapTR_loop___at___00__private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData_spec__0___closed__1));
|
||||
v___y_736_ = v___x_745_;
|
||||
goto v___jp_735_;
|
||||
}
|
||||
v___jp_735_:
|
||||
{
|
||||
lean_object* v___x_737_; lean_object* v___x_738_; lean_object* v___x_740_;
|
||||
v___x_737_ = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(v___x_737_, 0, v___y_736_);
|
||||
v___x_738_ = l_Lean_MessageData_ofFormat(v___x_737_);
|
||||
if (v_isShared_734_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_733_, 1, v_a_728_);
|
||||
lean_ctor_set(v___x_733_, 0, v___x_738_);
|
||||
v___x_740_ = v___x_733_;
|
||||
goto v_reusejp_739_;
|
||||
v___x_745_ = ((lean_object*)(l_List_mapTR_loop___at___00__private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData_spec__0___closed__0));
|
||||
v___y_737_ = v___x_745_;
|
||||
goto v___jp_736_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_742_;
|
||||
v_reuseFailAlloc_742_ = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(v_reuseFailAlloc_742_, 0, v___x_738_);
|
||||
lean_ctor_set(v_reuseFailAlloc_742_, 1, v_a_728_);
|
||||
v___x_740_ = v_reuseFailAlloc_742_;
|
||||
goto v_reusejp_739_;
|
||||
lean_object* v___x_746_;
|
||||
v___x_746_ = ((lean_object*)(l_List_mapTR_loop___at___00__private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData_spec__0___closed__1));
|
||||
v___y_737_ = v___x_746_;
|
||||
goto v___jp_736_;
|
||||
}
|
||||
v_reusejp_739_:
|
||||
v___jp_736_:
|
||||
{
|
||||
v_a_727_ = v_tail_731_;
|
||||
v_a_728_ = v___x_740_;
|
||||
lean_object* v___x_738_; lean_object* v___x_739_; lean_object* v___x_741_;
|
||||
v___x_738_ = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(v___x_738_, 0, v___y_737_);
|
||||
v___x_739_ = l_Lean_MessageData_ofFormat(v___x_738_);
|
||||
if (v_isShared_735_ == 0)
|
||||
{
|
||||
lean_ctor_set(v___x_734_, 1, v_a_729_);
|
||||
lean_ctor_set(v___x_734_, 0, v___x_739_);
|
||||
v___x_741_ = v___x_734_;
|
||||
goto v_reusejp_740_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_743_;
|
||||
v_reuseFailAlloc_743_ = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(v_reuseFailAlloc_743_, 0, v___x_739_);
|
||||
lean_ctor_set(v_reuseFailAlloc_743_, 1, v_a_729_);
|
||||
v___x_741_ = v_reuseFailAlloc_743_;
|
||||
goto v_reusejp_740_;
|
||||
}
|
||||
v_reusejp_740_:
|
||||
{
|
||||
v_a_728_ = v_tail_732_;
|
||||
v_a_729_ = v___x_741_;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
|
|
@ -2511,154 +2514,154 @@ goto _start;
|
|||
static lean_object* _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__2(void){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_750_; lean_object* v___x_751_;
|
||||
v___x_750_ = ((lean_object*)(l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__1));
|
||||
v___x_751_ = l_Lean_MessageData_ofFormat(v___x_750_);
|
||||
return v___x_751_;
|
||||
lean_object* v___x_751_; lean_object* v___x_752_;
|
||||
v___x_751_ = ((lean_object*)(l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__1));
|
||||
v___x_752_ = l_Lean_MessageData_ofFormat(v___x_751_);
|
||||
return v___x_752_;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__4(void){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_753_; lean_object* v___x_754_;
|
||||
v___x_753_ = ((lean_object*)(l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__3));
|
||||
v___x_754_ = l_Lean_stringToMessageData(v___x_753_);
|
||||
return v___x_754_;
|
||||
lean_object* v___x_754_; lean_object* v___x_755_;
|
||||
v___x_754_ = ((lean_object*)(l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__3));
|
||||
v___x_755_ = l_Lean_stringToMessageData(v___x_754_);
|
||||
return v___x_755_;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__6(void){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_756_; lean_object* v___x_757_;
|
||||
v___x_756_ = ((lean_object*)(l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__5));
|
||||
v___x_757_ = l_Lean_stringToMessageData(v___x_756_);
|
||||
return v___x_757_;
|
||||
lean_object* v___x_757_; lean_object* v___x_758_;
|
||||
v___x_757_ = ((lean_object*)(l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__5));
|
||||
v___x_758_ = l_Lean_stringToMessageData(v___x_757_);
|
||||
return v___x_758_;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__8(void){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_759_; lean_object* v___x_760_;
|
||||
v___x_759_ = ((lean_object*)(l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__7));
|
||||
v___x_760_ = l_Lean_stringToMessageData(v___x_759_);
|
||||
return v___x_760_;
|
||||
lean_object* v___x_760_; lean_object* v___x_761_;
|
||||
v___x_760_ = ((lean_object*)(l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__7));
|
||||
v___x_761_ = l_Lean_stringToMessageData(v___x_760_);
|
||||
return v___x_761_;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__10(void){
|
||||
_start:
|
||||
{
|
||||
lean_object* v___x_762_; lean_object* v___x_763_;
|
||||
v___x_762_ = ((lean_object*)(l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__9));
|
||||
v___x_763_ = l_Lean_stringToMessageData(v___x_762_);
|
||||
return v___x_763_;
|
||||
lean_object* v___x_763_; lean_object* v___x_764_;
|
||||
v___x_763_ = ((lean_object*)(l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__9));
|
||||
v___x_764_ = l_Lean_stringToMessageData(v___x_763_);
|
||||
return v___x_764_;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData(lean_object* v_x_764_){
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData(lean_object* v_x_765_){
|
||||
_start:
|
||||
{
|
||||
switch(lean_obj_tag(v_x_764_))
|
||||
switch(lean_obj_tag(v_x_765_))
|
||||
{
|
||||
case 0:
|
||||
{
|
||||
lean_object* v___x_765_;
|
||||
v___x_765_ = lean_obj_once(&l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__2, &l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__2_once, _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__2);
|
||||
return v___x_765_;
|
||||
lean_object* v___x_766_;
|
||||
v___x_766_ = lean_obj_once(&l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__2, &l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__2_once, _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__2);
|
||||
return v___x_766_;
|
||||
}
|
||||
case 1:
|
||||
{
|
||||
lean_object* v_prefixSize_766_; lean_object* v_suffixSize_767_; lean_object* v___x_769_; uint8_t v_isShared_770_; uint8_t v_isSharedCheck_784_;
|
||||
v_prefixSize_766_ = lean_ctor_get(v_x_764_, 0);
|
||||
v_suffixSize_767_ = lean_ctor_get(v_x_764_, 1);
|
||||
v_isSharedCheck_784_ = !lean_is_exclusive(v_x_764_);
|
||||
if (v_isSharedCheck_784_ == 0)
|
||||
lean_object* v_prefixSize_767_; lean_object* v_suffixSize_768_; lean_object* v___x_770_; uint8_t v_isShared_771_; uint8_t v_isSharedCheck_785_;
|
||||
v_prefixSize_767_ = lean_ctor_get(v_x_765_, 0);
|
||||
v_suffixSize_768_ = lean_ctor_get(v_x_765_, 1);
|
||||
v_isSharedCheck_785_ = !lean_is_exclusive(v_x_765_);
|
||||
if (v_isSharedCheck_785_ == 0)
|
||||
{
|
||||
v___x_769_ = v_x_764_;
|
||||
v_isShared_770_ = v_isSharedCheck_784_;
|
||||
goto v_resetjp_768_;
|
||||
v___x_770_ = v_x_765_;
|
||||
v_isShared_771_ = v_isSharedCheck_785_;
|
||||
goto v_resetjp_769_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_inc(v_suffixSize_767_);
|
||||
lean_inc(v_prefixSize_766_);
|
||||
lean_dec(v_x_764_);
|
||||
v___x_769_ = lean_box(0);
|
||||
v_isShared_770_ = v_isSharedCheck_784_;
|
||||
goto v_resetjp_768_;
|
||||
lean_inc(v_suffixSize_768_);
|
||||
lean_inc(v_prefixSize_767_);
|
||||
lean_dec(v_x_765_);
|
||||
v___x_770_ = lean_box(0);
|
||||
v_isShared_771_ = v_isSharedCheck_785_;
|
||||
goto v_resetjp_769_;
|
||||
}
|
||||
v_resetjp_768_:
|
||||
v_resetjp_769_:
|
||||
{
|
||||
lean_object* v___x_771_; lean_object* v___x_772_; lean_object* v___x_773_; lean_object* v___x_774_; lean_object* v___x_776_;
|
||||
v___x_771_ = lean_obj_once(&l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__4, &l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__4_once, _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__4);
|
||||
v___x_772_ = l_Nat_reprFast(v_prefixSize_766_);
|
||||
v___x_773_ = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(v___x_773_, 0, v___x_772_);
|
||||
v___x_774_ = l_Lean_MessageData_ofFormat(v___x_773_);
|
||||
if (v_isShared_770_ == 0)
|
||||
lean_object* v___x_772_; lean_object* v___x_773_; lean_object* v___x_774_; lean_object* v___x_775_; lean_object* v___x_777_;
|
||||
v___x_772_ = lean_obj_once(&l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__4, &l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__4_once, _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__4);
|
||||
v___x_773_ = l_Nat_reprFast(v_prefixSize_767_);
|
||||
v___x_774_ = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(v___x_774_, 0, v___x_773_);
|
||||
v___x_775_ = l_Lean_MessageData_ofFormat(v___x_774_);
|
||||
if (v_isShared_771_ == 0)
|
||||
{
|
||||
lean_ctor_set_tag(v___x_769_, 7);
|
||||
lean_ctor_set(v___x_769_, 1, v___x_774_);
|
||||
lean_ctor_set(v___x_769_, 0, v___x_771_);
|
||||
v___x_776_ = v___x_769_;
|
||||
goto v_reusejp_775_;
|
||||
lean_ctor_set_tag(v___x_770_, 7);
|
||||
lean_ctor_set(v___x_770_, 1, v___x_775_);
|
||||
lean_ctor_set(v___x_770_, 0, v___x_772_);
|
||||
v___x_777_ = v___x_770_;
|
||||
goto v_reusejp_776_;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* v_reuseFailAlloc_783_;
|
||||
v_reuseFailAlloc_783_ = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(v_reuseFailAlloc_783_, 0, v___x_771_);
|
||||
lean_ctor_set(v_reuseFailAlloc_783_, 1, v___x_774_);
|
||||
v___x_776_ = v_reuseFailAlloc_783_;
|
||||
goto v_reusejp_775_;
|
||||
lean_object* v_reuseFailAlloc_784_;
|
||||
v_reuseFailAlloc_784_ = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(v_reuseFailAlloc_784_, 0, v___x_772_);
|
||||
lean_ctor_set(v_reuseFailAlloc_784_, 1, v___x_775_);
|
||||
v___x_777_ = v_reuseFailAlloc_784_;
|
||||
goto v_reusejp_776_;
|
||||
}
|
||||
v_reusejp_775_:
|
||||
v_reusejp_776_:
|
||||
{
|
||||
lean_object* v___x_777_; lean_object* v___x_778_; lean_object* v___x_779_; lean_object* v___x_780_; lean_object* v___x_781_; lean_object* v___x_782_;
|
||||
v___x_777_ = lean_obj_once(&l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__6, &l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__6_once, _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__6);
|
||||
v___x_778_ = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(v___x_778_, 0, v___x_776_);
|
||||
lean_ctor_set(v___x_778_, 1, v___x_777_);
|
||||
v___x_779_ = l_Nat_reprFast(v_suffixSize_767_);
|
||||
v___x_780_ = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(v___x_780_, 0, v___x_779_);
|
||||
v___x_781_ = l_Lean_MessageData_ofFormat(v___x_780_);
|
||||
v___x_782_ = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(v___x_782_, 0, v___x_778_);
|
||||
lean_ctor_set(v___x_782_, 1, v___x_781_);
|
||||
return v___x_782_;
|
||||
lean_object* v___x_778_; lean_object* v___x_779_; lean_object* v___x_780_; lean_object* v___x_781_; lean_object* v___x_782_; lean_object* v___x_783_;
|
||||
v___x_778_ = lean_obj_once(&l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__6, &l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__6_once, _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__6);
|
||||
v___x_779_ = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(v___x_779_, 0, v___x_777_);
|
||||
lean_ctor_set(v___x_779_, 1, v___x_778_);
|
||||
v___x_780_ = l_Nat_reprFast(v_suffixSize_768_);
|
||||
v___x_781_ = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(v___x_781_, 0, v___x_780_);
|
||||
v___x_782_ = l_Lean_MessageData_ofFormat(v___x_781_);
|
||||
v___x_783_ = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(v___x_783_, 0, v___x_779_);
|
||||
lean_ctor_set(v___x_783_, 1, v___x_782_);
|
||||
return v___x_783_;
|
||||
}
|
||||
}
|
||||
}
|
||||
case 2:
|
||||
{
|
||||
lean_object* v_rewritable_785_; lean_object* v___x_786_; lean_object* v___x_787_; lean_object* v___x_788_; lean_object* v___x_789_; lean_object* v___x_790_; lean_object* v___x_791_;
|
||||
v_rewritable_785_ = lean_ctor_get(v_x_764_, 0);
|
||||
lean_inc_ref(v_rewritable_785_);
|
||||
lean_dec_ref(v_x_764_);
|
||||
v___x_786_ = lean_obj_once(&l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__8, &l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__8_once, _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__8);
|
||||
v___x_787_ = lean_array_to_list(v_rewritable_785_);
|
||||
v___x_788_ = lean_box(0);
|
||||
v___x_789_ = l_List_mapTR_loop___at___00__private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData_spec__0(v___x_787_, v___x_788_);
|
||||
v___x_790_ = l_Lean_MessageData_ofList(v___x_789_);
|
||||
v___x_791_ = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(v___x_791_, 0, v___x_786_);
|
||||
lean_ctor_set(v___x_791_, 1, v___x_790_);
|
||||
return v___x_791_;
|
||||
lean_object* v_rewritable_786_; lean_object* v___x_787_; lean_object* v___x_788_; lean_object* v___x_789_; lean_object* v___x_790_; lean_object* v___x_791_; lean_object* v___x_792_;
|
||||
v_rewritable_786_ = lean_ctor_get(v_x_765_, 0);
|
||||
lean_inc_ref(v_rewritable_786_);
|
||||
lean_dec_ref(v_x_765_);
|
||||
v___x_787_ = lean_obj_once(&l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__8, &l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__8_once, _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__8);
|
||||
v___x_788_ = lean_array_to_list(v_rewritable_786_);
|
||||
v___x_789_ = lean_box(0);
|
||||
v___x_790_ = l_List_mapTR_loop___at___00__private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData_spec__0(v___x_788_, v___x_789_);
|
||||
v___x_791_ = l_Lean_MessageData_ofList(v___x_790_);
|
||||
v___x_792_ = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(v___x_792_, 0, v___x_787_);
|
||||
lean_ctor_set(v___x_792_, 1, v___x_791_);
|
||||
return v___x_792_;
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* v_thm_792_; lean_object* v_proof_793_; lean_object* v___x_794_; lean_object* v___x_795_; lean_object* v___x_796_;
|
||||
v_thm_792_ = lean_ctor_get(v_x_764_, 0);
|
||||
lean_inc_ref(v_thm_792_);
|
||||
lean_dec_ref(v_x_764_);
|
||||
v_proof_793_ = lean_ctor_get(v_thm_792_, 1);
|
||||
lean_inc_ref(v_proof_793_);
|
||||
lean_dec_ref(v_thm_792_);
|
||||
v___x_794_ = lean_obj_once(&l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__10, &l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__10_once, _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__10);
|
||||
v___x_795_ = l_Lean_MessageData_ofExpr(v_proof_793_);
|
||||
v___x_796_ = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(v___x_796_, 0, v___x_794_);
|
||||
lean_ctor_set(v___x_796_, 1, v___x_795_);
|
||||
return v___x_796_;
|
||||
lean_object* v_thm_793_; lean_object* v_proof_794_; lean_object* v___x_795_; lean_object* v___x_796_; lean_object* v___x_797_;
|
||||
v_thm_793_ = lean_ctor_get(v_x_765_, 0);
|
||||
lean_inc_ref(v_thm_793_);
|
||||
lean_dec_ref(v_x_765_);
|
||||
v_proof_794_ = lean_ctor_get(v_thm_793_, 1);
|
||||
lean_inc_ref(v_proof_794_);
|
||||
lean_dec_ref(v_thm_793_);
|
||||
v___x_795_ = lean_obj_once(&l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__10, &l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__10_once, _init_l___private_Lean_Meta_Sym_Simp_CongrInfo_0__Lean_Meta_Sym_CongrInfo_toMessageData___closed__10);
|
||||
v___x_796_ = l_Lean_MessageData_ofExpr(v_proof_794_);
|
||||
v___x_797_ = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(v___x_797_, 0, v___x_795_);
|
||||
lean_ctor_set(v___x_797_, 1, v___x_796_);
|
||||
return v___x_797_;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
2
stage0/stdlib/Lean/Meta/Sym/Simp/ControlFlow.c
generated
2
stage0/stdlib/Lean/Meta/Sym/Simp/ControlFlow.c
generated
|
|
@ -230,7 +230,7 @@ _start:
|
|||
{
|
||||
lean_object* v___y_11_; lean_object* v___x_14_; uint8_t v_debug_15_;
|
||||
v___x_14_ = lean_st_ref_get(v___y_4_);
|
||||
v_debug_15_ = lean_ctor_get_uint8(v___x_14_, sizeof(void*)*7);
|
||||
v_debug_15_ = lean_ctor_get_uint8(v___x_14_, sizeof(void*)*8);
|
||||
lean_dec(v___x_14_);
|
||||
if (v_debug_15_ == 0)
|
||||
{
|
||||
|
|
|
|||
8
stage0/stdlib/Lean/Meta/Sym/Simp/Forall.c
generated
8
stage0/stdlib/Lean/Meta/Sym/Simp/Forall.c
generated
|
|
@ -1288,7 +1288,7 @@ _start:
|
|||
{
|
||||
lean_object* v___y_538_; lean_object* v___x_541_; uint8_t v_debug_542_;
|
||||
v___x_541_ = lean_st_ref_get(v___y_531_);
|
||||
v_debug_542_ = lean_ctor_get_uint8(v___x_541_, sizeof(void*)*7);
|
||||
v_debug_542_ = lean_ctor_get_uint8(v___x_541_, sizeof(void*)*8);
|
||||
lean_dec(v___x_541_);
|
||||
if (v_debug_542_ == 0)
|
||||
{
|
||||
|
|
@ -1895,7 +1895,7 @@ _start:
|
|||
{
|
||||
lean_object* v___y_715_; lean_object* v___x_718_; uint8_t v_debug_719_;
|
||||
v___x_718_ = lean_st_ref_get(v___y_708_);
|
||||
v_debug_719_ = lean_ctor_get_uint8(v___x_718_, sizeof(void*)*7);
|
||||
v_debug_719_ = lean_ctor_get_uint8(v___x_718_, sizeof(void*)*8);
|
||||
lean_dec(v___x_718_);
|
||||
if (v_debug_719_ == 0)
|
||||
{
|
||||
|
|
@ -2152,7 +2152,7 @@ _start:
|
|||
{
|
||||
lean_object* v___y_800_; lean_object* v___x_803_; uint8_t v_debug_804_;
|
||||
v___x_803_ = lean_st_ref_get(v___y_793_);
|
||||
v_debug_804_ = lean_ctor_get_uint8(v___x_803_, sizeof(void*)*7);
|
||||
v_debug_804_ = lean_ctor_get_uint8(v___x_803_, sizeof(void*)*8);
|
||||
lean_dec(v___x_803_);
|
||||
if (v_debug_804_ == 0)
|
||||
{
|
||||
|
|
@ -5056,7 +5056,7 @@ _start:
|
|||
{
|
||||
lean_object* v___y_1587_; lean_object* v___x_1590_; uint8_t v_debug_1591_;
|
||||
v___x_1590_ = lean_st_ref_get(v___y_1580_);
|
||||
v_debug_1591_ = lean_ctor_get_uint8(v___x_1590_, sizeof(void*)*7);
|
||||
v_debug_1591_ = lean_ctor_get_uint8(v___x_1590_, sizeof(void*)*8);
|
||||
lean_dec(v___x_1590_);
|
||||
if (v_debug_1591_ == 0)
|
||||
{
|
||||
|
|
|
|||
11782
stage0/stdlib/Lean/Meta/Sym/Simp/Have.c
generated
11782
stage0/stdlib/Lean/Meta/Sym/Simp/Have.c
generated
File diff suppressed because it is too large
Load diff
2
stage0/stdlib/Lean/Meta/Sym/Simp/Main.c
generated
2
stage0/stdlib/Lean/Meta/Sym/Simp/Main.c
generated
|
|
@ -329,7 +329,7 @@ _start:
|
|||
{
|
||||
lean_object* v___y_103_; lean_object* v___x_106_; uint8_t v_debug_107_;
|
||||
v___x_106_ = lean_st_ref_get(v___y_96_);
|
||||
v_debug_107_ = lean_ctor_get_uint8(v___x_106_, sizeof(void*)*7);
|
||||
v_debug_107_ = lean_ctor_get_uint8(v___x_106_, sizeof(void*)*8);
|
||||
lean_dec(v___x_106_);
|
||||
if (v_debug_107_ == 0)
|
||||
{
|
||||
|
|
|
|||
5898
stage0/stdlib/Lean/Meta/Sym/SymM.c
generated
5898
stage0/stdlib/Lean/Meta/Sym/SymM.c
generated
File diff suppressed because it is too large
Load diff
2
stage0/stdlib/Lean/Meta/Tactic/Cbv/ControlFlow.c
generated
2
stage0/stdlib/Lean/Meta/Tactic/Cbv/ControlFlow.c
generated
|
|
@ -2347,7 +2347,7 @@ _start:
|
|||
{
|
||||
lean_object* v___y_571_; lean_object* v___x_574_; uint8_t v_debug_575_;
|
||||
v___x_574_ = lean_st_ref_get(v___y_564_);
|
||||
v_debug_575_ = lean_ctor_get_uint8(v___x_574_, sizeof(void*)*7);
|
||||
v_debug_575_ = lean_ctor_get_uint8(v___x_574_, sizeof(void*)*8);
|
||||
lean_dec(v___x_574_);
|
||||
if (v_debug_575_ == 0)
|
||||
{
|
||||
|
|
|
|||
2
stage0/stdlib/Lean/Meta/Tactic/Cbv/Main.c
generated
2
stage0/stdlib/Lean/Meta/Tactic/Cbv/Main.c
generated
|
|
@ -14146,7 +14146,7 @@ _start:
|
|||
{
|
||||
lean_object* v___y_4634_; lean_object* v___x_4637_; uint8_t v_debug_4638_;
|
||||
v___x_4637_ = lean_st_ref_get(v___y_4627_);
|
||||
v_debug_4638_ = lean_ctor_get_uint8(v___x_4637_, sizeof(void*)*7);
|
||||
v_debug_4638_ = lean_ctor_get_uint8(v___x_4637_, sizeof(void*)*8);
|
||||
lean_dec(v___x_4637_);
|
||||
if (v_debug_4638_ == 0)
|
||||
{
|
||||
|
|
|
|||
2
stage0/stdlib/Lean/Meta/Tactic/Cbv/Util.c
generated
2
stage0/stdlib/Lean/Meta/Tactic/Cbv/Util.c
generated
|
|
@ -215,7 +215,7 @@ _start:
|
|||
{
|
||||
lean_object* v___y_11_; lean_object* v___x_14_; uint8_t v_debug_15_;
|
||||
v___x_14_ = lean_st_ref_get(v___y_4_);
|
||||
v_debug_15_ = lean_ctor_get_uint8(v___x_14_, sizeof(void*)*7);
|
||||
v_debug_15_ = lean_ctor_get_uint8(v___x_14_, sizeof(void*)*8);
|
||||
lean_dec(v___x_14_);
|
||||
if (v_debug_15_ == 0)
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue