chore(boot): update
This commit is contained in:
Leonardo de Moura
parent
7c355d3ba6
commit
16f6da6a62
4 changed files with 251 additions and 353 deletions
|
|
@ -13,7 +13,6 @@ typedef lean::object obj;
|
|||
obj* l_psum_sizeof(obj*, obj*);
|
||||
obj* l_sigma_sizeof___main___rarg(obj*, obj*, obj*);
|
||||
obj* l_eq_ndrec__on___rarg(obj*);
|
||||
obj* l_thunk_map(obj*, obj*);
|
||||
obj* l_bool_has__sizeof;
|
||||
obj* l_quot_rec__on__subsingleton___rarg(obj*, obj*);
|
||||
obj* l_total;
|
||||
|
|
@ -21,13 +20,11 @@ obj* l_implies_decidable___rarg(obj*, obj*);
|
|||
obj* l_psigma_has__sizeof(obj*, obj*);
|
||||
obj* l_nat_add___main(obj*, obj*);
|
||||
obj* l_quotient_rec__on__subsingleton_u_2082___at_quotient_decidable__eq___spec__1___rarg(obj*, obj*, obj*);
|
||||
obj* l_thunk_bind___rarg(obj*, obj*, unsigned char);
|
||||
obj* l_eq_ndrec(obj*, obj*, obj*);
|
||||
obj* l_prod_inhabited___rarg(obj*, obj*);
|
||||
obj* l_prod_sizeof___main(obj*, obj*);
|
||||
obj* l_subtype_inhabited___rarg(obj*, obj*);
|
||||
obj* l_decidable_to__bool(obj*);
|
||||
obj* l_thunk_pure___rarg___boxed(obj*, obj*);
|
||||
obj* l_sum_sizeof___main(obj*, obj*);
|
||||
obj* l_punit_sizeof(unsigned char);
|
||||
obj* l_inline(obj*);
|
||||
|
|
@ -57,7 +54,6 @@ obj* l_prod_sizeof(obj*, obj*);
|
|||
unsigned char l_bxor___main(unsigned char, unsigned char);
|
||||
unsigned char l_unit_star;
|
||||
obj* l_exists_intro;
|
||||
obj* l_thunk_map___rarg(obj*, obj*, unsigned char);
|
||||
obj* l___private_2312050019__extfun__app(obj*, obj*);
|
||||
obj* l_or_intro__right;
|
||||
obj* l_bit1(obj*);
|
||||
|
|
@ -107,7 +103,6 @@ obj* l_false_elim___boxed(obj*, obj*);
|
|||
unsigned char l_band(unsigned char, unsigned char);
|
||||
obj* l_false_elim(obj*, unsigned char);
|
||||
obj* l_std_priority_max;
|
||||
obj* l_thunk_pure(obj*);
|
||||
obj* l_punit_sizeof___main(unsigned char);
|
||||
unsigned char l_bor(unsigned char, unsigned char);
|
||||
obj* l_option_sizeof___main(obj*);
|
||||
|
|
@ -124,7 +119,6 @@ obj* l_psum_sizeof___main___rarg(obj*, obj*, obj*);
|
|||
obj* l_subrelation;
|
||||
obj* l_quot_rec__on___rarg(obj*, obj*, obj*);
|
||||
obj* l_bor___boxed(obj*, obj*);
|
||||
obj* l_thunk_bind(obj*, obj*);
|
||||
obj* l_ite(obj*);
|
||||
obj* l_eq_ndrec___rarg(obj*, obj*, obj*);
|
||||
obj* l_or_by__cases___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
|
||||
|
|
@ -140,7 +134,6 @@ obj* l_sum_sizeof(obj*, obj*);
|
|||
obj* l_type__eq__of__heq;
|
||||
obj* l_inv__image;
|
||||
obj* l_punit_subsingleton;
|
||||
obj* l_thunk_get___rarg(obj*);
|
||||
obj* l_bool_inhabited___boxed;
|
||||
obj* l_list_sizeof___main(obj*);
|
||||
obj* l_xor;
|
||||
|
|
@ -197,7 +190,6 @@ obj* l_iff_decidable___rarg(obj*, obj*);
|
|||
obj* l_std_prec_max__plus;
|
||||
obj* l_bit0(obj*);
|
||||
obj* l_exists__prop__decidable___rarg(obj*, obj*);
|
||||
obj* l_thunk_bind___rarg___boxed(obj*, obj*, obj*);
|
||||
obj* l_prod_has__sizeof(obj*, obj*);
|
||||
obj* l_decidable_rec__on__true___rarg(obj*, obj*, obj*, obj*, obj*);
|
||||
obj* l_decidable_to__bool___rarg___boxed(obj*);
|
||||
|
|
@ -247,7 +239,6 @@ obj* l_sigma_has__sizeof___rarg(obj*, obj*);
|
|||
obj* l_true_inhabited;
|
||||
obj* l_pi_subsingleton;
|
||||
obj* l_forall__prop__decidable___rarg(obj*, obj*);
|
||||
obj* l_thunk_get(obj*);
|
||||
obj* l_ne_decidable___rarg(obj*, obj*, obj*);
|
||||
obj* l_and__implies;
|
||||
obj* l_anti__symmetric;
|
||||
|
|
@ -286,7 +277,6 @@ obj* l_psigma_sizeof___main___at_psigma_has__sizeof___spec__2(obj*, obj*);
|
|||
obj* l_quotient_mk(obj*, obj*);
|
||||
obj* l_typed__expr(obj*);
|
||||
obj* l_not_decidable(obj*);
|
||||
obj* l_thunk_pure___rarg(obj*, unsigned char);
|
||||
obj* l_sum_decidable__eq___rarg(obj*, obj*, obj*, obj*);
|
||||
obj* l_cast(obj*, obj*, obj*);
|
||||
obj* l_quotient_decidable__eq(obj*);
|
||||
|
|
@ -354,7 +344,6 @@ obj* l_prod_map___rarg(obj*, obj*, obj*);
|
|||
obj* l_subsingleton_helim;
|
||||
obj* l_id__rhs___rarg(obj*);
|
||||
unsigned char l_bnot(unsigned char);
|
||||
obj* l_thunk_map___rarg___boxed(obj*, obj*, obj*);
|
||||
obj* l_decidable_by__cases___rarg(obj*, obj*, obj*);
|
||||
obj* l_decidable__of__decidable__of__iff(obj*, obj*);
|
||||
obj* l_right__commutative;
|
||||
|
|
@ -519,106 +508,6 @@ x_1 = lean::box(x_0);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_pure___rarg(obj* x_0, unsigned char x_1) {
|
||||
_start:
|
||||
{
|
||||
return x_0;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_pure(obj* x_0) {
|
||||
_start:
|
||||
{
|
||||
obj* x_2;
|
||||
lean::dec(x_0);
|
||||
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_thunk_pure___rarg___boxed), 2, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_pure___rarg___boxed(obj* x_0, obj* x_1) {
|
||||
_start:
|
||||
{
|
||||
unsigned char x_2; obj* x_3;
|
||||
x_2 = lean::unbox(x_1);
|
||||
x_3 = l_thunk_pure___rarg(x_0, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_get___rarg(obj* x_0) {
|
||||
_start:
|
||||
{
|
||||
unsigned char x_1; obj* x_2; obj* x_3;
|
||||
x_1 = 0;
|
||||
x_2 = lean::box(x_1);
|
||||
x_3 = lean::apply_1(x_0, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_get(obj* x_0) {
|
||||
_start:
|
||||
{
|
||||
obj* x_2;
|
||||
lean::dec(x_0);
|
||||
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_thunk_get___rarg), 1, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_map___rarg(obj* x_0, obj* x_1, unsigned char x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_3; obj* x_4;
|
||||
x_3 = l_thunk_get___rarg(x_1);
|
||||
x_4 = lean::apply_1(x_0, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_map(obj* x_0, obj* x_1) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_0);
|
||||
x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_thunk_map___rarg___boxed), 3, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_map___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
unsigned char x_3; obj* x_4;
|
||||
x_3 = lean::unbox(x_2);
|
||||
x_4 = l_thunk_map___rarg(x_0, x_1, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_bind___rarg(obj* x_0, obj* x_1, unsigned char x_2) {
|
||||
_start:
|
||||
{
|
||||
obj* x_3; obj* x_4; obj* x_5;
|
||||
x_3 = l_thunk_get___rarg(x_0);
|
||||
x_4 = lean::apply_1(x_1, x_3);
|
||||
x_5 = l_thunk_get___rarg(x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_bind(obj* x_0, obj* x_1) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4;
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_0);
|
||||
x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_thunk_bind___rarg___boxed), 3, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_thunk_bind___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
|
||||
_start:
|
||||
{
|
||||
unsigned char x_3; obj* x_4;
|
||||
x_3 = lean::unbox(x_2);
|
||||
x_4 = l_thunk_bind___rarg(x_0, x_1, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
obj* l_task_pure___rarg(obj* x_0, unsigned char x_1) {
|
||||
_start:
|
||||
{
|
||||
|
|
|
|||
|
|
@ -54,7 +54,6 @@ obj* l_lean_format_sbracket___closed__1;
|
|||
obj* l_lean_format_repr___main___closed__6;
|
||||
obj* l_lean_format_sbracket(obj*);
|
||||
obj* l_lean_prod__has__to__format(obj*, obj*);
|
||||
obj* l_thunk_get___rarg(obj*);
|
||||
obj* l_lean_format_space__upto__line_x_27___main___lambda__1(obj*, obj*, unsigned char);
|
||||
obj* l_lean_nat__has__to__format(obj*);
|
||||
obj* l_lean_string__has__to__format(obj*);
|
||||
|
|
@ -375,53 +374,54 @@ return x_1;
|
|||
}
|
||||
lbl_4:
|
||||
{
|
||||
obj* x_13; unsigned char x_14;
|
||||
x_13 = l_thunk_get___rarg(x_2);
|
||||
x_14 = lean::cnstr_get_scalar<unsigned char>(x_13, sizeof(void*)*1 + 1);
|
||||
if (x_14 == 0)
|
||||
{
|
||||
unsigned char x_15;
|
||||
x_15 = lean::cnstr_get_scalar<unsigned char>(x_13, sizeof(void*)*1);
|
||||
obj* x_13; unsigned char x_15;
|
||||
x_13 = lean::thunk_get(x_2);
|
||||
lean::dec(x_2);
|
||||
x_15 = lean::cnstr_get_scalar<unsigned char>(x_13, sizeof(void*)*1 + 1);
|
||||
if (x_15 == 0)
|
||||
{
|
||||
obj* x_16; obj* x_19; obj* x_22; obj* x_25;
|
||||
x_16 = lean::cnstr_get(x_1, 0);
|
||||
lean::inc(x_16);
|
||||
lean::dec(x_1);
|
||||
x_19 = lean::cnstr_get(x_13, 0);
|
||||
lean::inc(x_19);
|
||||
lean::dec(x_13);
|
||||
x_22 = lean::nat_add(x_16, x_19);
|
||||
lean::dec(x_19);
|
||||
lean::dec(x_16);
|
||||
x_25 = lean::nat_dec_lt(x_0, x_22);
|
||||
lean::dec(x_0);
|
||||
if (lean::obj_tag(x_25) == 0)
|
||||
unsigned char x_16;
|
||||
x_16 = lean::cnstr_get_scalar<unsigned char>(x_13, sizeof(void*)*1);
|
||||
if (x_16 == 0)
|
||||
{
|
||||
unsigned char x_28; obj* x_29; obj* x_30; obj* x_31;
|
||||
lean::dec(x_25);
|
||||
x_28 = 0;
|
||||
x_29 = lean::alloc_cnstr(0, 1, 2);
|
||||
lean::cnstr_set(x_29, 0, x_22);
|
||||
lean::cnstr_set_scalar(x_29, sizeof(void*)*1, x_28);
|
||||
x_30 = x_29;
|
||||
lean::cnstr_set_scalar(x_30, sizeof(void*)*1 + 1, x_28);
|
||||
obj* x_17; obj* x_20; obj* x_23; obj* x_26;
|
||||
x_17 = lean::cnstr_get(x_1, 0);
|
||||
lean::inc(x_17);
|
||||
lean::dec(x_1);
|
||||
x_20 = lean::cnstr_get(x_13, 0);
|
||||
lean::inc(x_20);
|
||||
lean::dec(x_13);
|
||||
x_23 = lean::nat_add(x_17, x_20);
|
||||
lean::dec(x_20);
|
||||
lean::dec(x_17);
|
||||
x_26 = lean::nat_dec_lt(x_0, x_23);
|
||||
lean::dec(x_0);
|
||||
if (lean::obj_tag(x_26) == 0)
|
||||
{
|
||||
unsigned char x_29; obj* x_30; obj* x_31; obj* x_32;
|
||||
lean::dec(x_26);
|
||||
x_29 = 0;
|
||||
x_30 = lean::alloc_cnstr(0, 1, 2);
|
||||
lean::cnstr_set(x_30, 0, x_23);
|
||||
lean::cnstr_set_scalar(x_30, sizeof(void*)*1, x_29);
|
||||
x_31 = x_30;
|
||||
return x_31;
|
||||
lean::cnstr_set_scalar(x_31, sizeof(void*)*1 + 1, x_29);
|
||||
x_32 = x_31;
|
||||
return x_32;
|
||||
}
|
||||
else
|
||||
{
|
||||
unsigned char x_33; unsigned char x_34; obj* x_35; obj* x_36; obj* x_37;
|
||||
lean::dec(x_25);
|
||||
x_33 = 0;
|
||||
x_34 = 1;
|
||||
x_35 = lean::alloc_cnstr(0, 1, 2);
|
||||
lean::cnstr_set(x_35, 0, x_22);
|
||||
lean::cnstr_set_scalar(x_35, sizeof(void*)*1, x_33);
|
||||
x_36 = x_35;
|
||||
lean::cnstr_set_scalar(x_36, sizeof(void*)*1 + 1, x_34);
|
||||
unsigned char x_34; unsigned char x_35; obj* x_36; obj* x_37; obj* x_38;
|
||||
lean::dec(x_26);
|
||||
x_34 = 0;
|
||||
x_35 = 1;
|
||||
x_36 = lean::alloc_cnstr(0, 1, 2);
|
||||
lean::cnstr_set(x_36, 0, x_23);
|
||||
lean::cnstr_set_scalar(x_36, sizeof(void*)*1, x_34);
|
||||
x_37 = x_36;
|
||||
return x_37;
|
||||
lean::cnstr_set_scalar(x_37, sizeof(void*)*1 + 1, x_35);
|
||||
x_38 = x_37;
|
||||
return x_38;
|
||||
}
|
||||
}
|
||||
else
|
||||
|
|
@ -433,46 +433,46 @@ return x_13;
|
|||
}
|
||||
else
|
||||
{
|
||||
if (x_14 == 0)
|
||||
if (x_15 == 0)
|
||||
{
|
||||
obj* x_40; obj* x_43; obj* x_46; obj* x_49;
|
||||
x_40 = lean::cnstr_get(x_1, 0);
|
||||
lean::inc(x_40);
|
||||
obj* x_41; obj* x_44; obj* x_47; obj* x_50;
|
||||
x_41 = lean::cnstr_get(x_1, 0);
|
||||
lean::inc(x_41);
|
||||
lean::dec(x_1);
|
||||
x_43 = lean::cnstr_get(x_13, 0);
|
||||
lean::inc(x_43);
|
||||
x_44 = lean::cnstr_get(x_13, 0);
|
||||
lean::inc(x_44);
|
||||
lean::dec(x_13);
|
||||
x_46 = lean::nat_add(x_40, x_43);
|
||||
lean::dec(x_43);
|
||||
lean::dec(x_40);
|
||||
x_49 = lean::nat_dec_lt(x_0, x_46);
|
||||
x_47 = lean::nat_add(x_41, x_44);
|
||||
lean::dec(x_44);
|
||||
lean::dec(x_41);
|
||||
x_50 = lean::nat_dec_lt(x_0, x_47);
|
||||
lean::dec(x_0);
|
||||
if (lean::obj_tag(x_49) == 0)
|
||||
if (lean::obj_tag(x_50) == 0)
|
||||
{
|
||||
unsigned char x_52; obj* x_53; obj* x_54; obj* x_55;
|
||||
lean::dec(x_49);
|
||||
x_52 = 0;
|
||||
x_53 = lean::alloc_cnstr(0, 1, 2);
|
||||
lean::cnstr_set(x_53, 0, x_46);
|
||||
lean::cnstr_set_scalar(x_53, sizeof(void*)*1, x_52);
|
||||
x_54 = x_53;
|
||||
lean::cnstr_set_scalar(x_54, sizeof(void*)*1 + 1, x_52);
|
||||
unsigned char x_53; obj* x_54; obj* x_55; obj* x_56;
|
||||
lean::dec(x_50);
|
||||
x_53 = 0;
|
||||
x_54 = lean::alloc_cnstr(0, 1, 2);
|
||||
lean::cnstr_set(x_54, 0, x_47);
|
||||
lean::cnstr_set_scalar(x_54, sizeof(void*)*1, x_53);
|
||||
x_55 = x_54;
|
||||
return x_55;
|
||||
lean::cnstr_set_scalar(x_55, sizeof(void*)*1 + 1, x_53);
|
||||
x_56 = x_55;
|
||||
return x_56;
|
||||
}
|
||||
else
|
||||
{
|
||||
unsigned char x_57; unsigned char x_58; obj* x_59; obj* x_60; obj* x_61;
|
||||
lean::dec(x_49);
|
||||
x_57 = 0;
|
||||
x_58 = 1;
|
||||
x_59 = lean::alloc_cnstr(0, 1, 2);
|
||||
lean::cnstr_set(x_59, 0, x_46);
|
||||
lean::cnstr_set_scalar(x_59, sizeof(void*)*1, x_57);
|
||||
x_60 = x_59;
|
||||
lean::cnstr_set_scalar(x_60, sizeof(void*)*1 + 1, x_58);
|
||||
unsigned char x_58; unsigned char x_59; obj* x_60; obj* x_61; obj* x_62;
|
||||
lean::dec(x_50);
|
||||
x_58 = 0;
|
||||
x_59 = 1;
|
||||
x_60 = lean::alloc_cnstr(0, 1, 2);
|
||||
lean::cnstr_set(x_60, 0, x_47);
|
||||
lean::cnstr_set_scalar(x_60, sizeof(void*)*1, x_58);
|
||||
x_61 = x_60;
|
||||
return x_61;
|
||||
lean::cnstr_set_scalar(x_61, sizeof(void*)*1 + 1, x_59);
|
||||
x_62 = x_61;
|
||||
return x_62;
|
||||
}
|
||||
}
|
||||
else
|
||||
|
|
@ -556,7 +556,7 @@ goto _start;
|
|||
}
|
||||
case 4:
|
||||
{
|
||||
obj* x_32; obj* x_34; obj* x_38; obj* x_40; obj* x_41;
|
||||
obj* x_32; obj* x_34; obj* x_38; obj* x_40; obj* x_41; obj* x_42;
|
||||
x_32 = lean::cnstr_get(x_0, 0);
|
||||
lean::inc(x_32);
|
||||
x_34 = lean::cnstr_get(x_0, 1);
|
||||
|
|
@ -568,16 +568,17 @@ lean::inc(x_1);
|
|||
x_40 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_format_space__upto__line___main___lambda__1___boxed), 3, 2);
|
||||
lean::closure_set(x_40, 0, x_34);
|
||||
lean::closure_set(x_40, 1, x_1);
|
||||
x_41 = l___private_3682637481__merge(x_1, x_38, x_40);
|
||||
return x_41;
|
||||
x_41 = lean::mk_thunk(x_40);
|
||||
x_42 = l___private_3682637481__merge(x_1, x_38, x_41);
|
||||
return x_42;
|
||||
}
|
||||
default:
|
||||
{
|
||||
obj* x_42;
|
||||
x_42 = lean::cnstr_get(x_0, 1);
|
||||
lean::inc(x_42);
|
||||
obj* x_43;
|
||||
x_43 = lean::cnstr_get(x_0, 1);
|
||||
lean::inc(x_43);
|
||||
lean::dec(x_0);
|
||||
x_0 = x_42;
|
||||
x_0 = x_43;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
|
|
@ -653,7 +654,7 @@ return x_4;
|
|||
}
|
||||
else
|
||||
{
|
||||
obj* x_6; obj* x_8; obj* x_11; obj* x_15; obj* x_17; obj* x_18;
|
||||
obj* x_6; obj* x_8; obj* x_11; obj* x_15; obj* x_17; obj* x_18; obj* x_19;
|
||||
x_6 = lean::cnstr_get(x_0, 0);
|
||||
lean::inc(x_6);
|
||||
x_8 = lean::cnstr_get(x_0, 1);
|
||||
|
|
@ -668,8 +669,9 @@ lean::inc(x_1);
|
|||
x_17 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_format_space__upto__line_x_27___main___lambda__1___boxed), 3, 2);
|
||||
lean::closure_set(x_17, 0, x_8);
|
||||
lean::closure_set(x_17, 1, x_1);
|
||||
x_18 = l___private_3682637481__merge(x_1, x_15, x_17);
|
||||
return x_18;
|
||||
x_18 = lean::mk_thunk(x_17);
|
||||
x_19 = l___private_3682637481__merge(x_1, x_15, x_18);
|
||||
return x_19;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -913,7 +915,7 @@ goto _start;
|
|||
}
|
||||
default:
|
||||
{
|
||||
obj* x_103; obj* x_105; obj* x_110; obj* x_113; obj* x_115; unsigned char x_116;
|
||||
obj* x_103; obj* x_105; obj* x_110; obj* x_113; obj* x_114; obj* x_116; unsigned char x_117;
|
||||
x_103 = lean::cnstr_get(x_14, 0);
|
||||
lean::inc(x_103);
|
||||
x_105 = lean::cnstr_get(x_14, 1);
|
||||
|
|
@ -927,50 +929,51 @@ lean::inc(x_9);
|
|||
x_113 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_format_space__upto__line_x_27___main___lambda__1___boxed), 3, 2);
|
||||
lean::closure_set(x_113, 0, x_9);
|
||||
lean::closure_set(x_113, 1, x_0);
|
||||
x_114 = lean::mk_thunk(x_113);
|
||||
lean::inc(x_0);
|
||||
x_115 = l___private_3682637481__merge(x_0, x_110, x_113);
|
||||
x_116 = lean::cnstr_get_scalar<unsigned char>(x_115, sizeof(void*)*1 + 1);
|
||||
lean::dec(x_115);
|
||||
if (x_116 == 0)
|
||||
x_116 = l___private_3682637481__merge(x_0, x_110, x_114);
|
||||
x_117 = lean::cnstr_get_scalar<unsigned char>(x_116, sizeof(void*)*1 + 1);
|
||||
lean::dec(x_116);
|
||||
if (x_117 == 0)
|
||||
{
|
||||
obj* x_119; obj* x_120;
|
||||
obj* x_120; obj* x_121;
|
||||
lean::dec(x_105);
|
||||
if (lean::is_scalar(x_16)) {
|
||||
x_119 = lean::alloc_cnstr(0, 2, 0);
|
||||
x_120 = lean::alloc_cnstr(0, 2, 0);
|
||||
} else {
|
||||
x_119 = x_16;
|
||||
x_120 = x_16;
|
||||
}
|
||||
lean::cnstr_set(x_119, 0, x_12);
|
||||
lean::cnstr_set(x_119, 1, x_103);
|
||||
lean::cnstr_set(x_120, 0, x_12);
|
||||
lean::cnstr_set(x_120, 1, x_103);
|
||||
if (lean::is_scalar(x_11)) {
|
||||
x_120 = lean::alloc_cnstr(1, 2, 0);
|
||||
x_121 = lean::alloc_cnstr(1, 2, 0);
|
||||
} else {
|
||||
x_120 = x_11;
|
||||
x_121 = x_11;
|
||||
}
|
||||
lean::cnstr_set(x_120, 0, x_119);
|
||||
lean::cnstr_set(x_120, 1, x_9);
|
||||
x_3 = x_120;
|
||||
lean::cnstr_set(x_121, 0, x_120);
|
||||
lean::cnstr_set(x_121, 1, x_9);
|
||||
x_3 = x_121;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_123; obj* x_124;
|
||||
obj* x_124; obj* x_125;
|
||||
lean::dec(x_103);
|
||||
if (lean::is_scalar(x_16)) {
|
||||
x_123 = lean::alloc_cnstr(0, 2, 0);
|
||||
x_124 = lean::alloc_cnstr(0, 2, 0);
|
||||
} else {
|
||||
x_123 = x_16;
|
||||
x_124 = x_16;
|
||||
}
|
||||
lean::cnstr_set(x_123, 0, x_12);
|
||||
lean::cnstr_set(x_123, 1, x_105);
|
||||
lean::cnstr_set(x_124, 0, x_12);
|
||||
lean::cnstr_set(x_124, 1, x_105);
|
||||
if (lean::is_scalar(x_11)) {
|
||||
x_124 = lean::alloc_cnstr(1, 2, 0);
|
||||
x_125 = lean::alloc_cnstr(1, 2, 0);
|
||||
} else {
|
||||
x_124 = x_11;
|
||||
x_125 = x_11;
|
||||
}
|
||||
lean::cnstr_set(x_124, 0, x_123);
|
||||
lean::cnstr_set(x_124, 1, x_9);
|
||||
x_3 = x_124;
|
||||
lean::cnstr_set(x_125, 0, x_124);
|
||||
lean::cnstr_set(x_125, 1, x_9);
|
||||
x_3 = x_125;
|
||||
goto _start;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -36,7 +36,6 @@ obj* l_lean_trace_trace__map;
|
|||
obj* l_lean_trace_lean_trace_monad__tracer(obj*);
|
||||
extern obj* l_lean_format_join___closed__1;
|
||||
obj* l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2(obj*, obj*, obj*);
|
||||
obj* l_thunk_get___rarg(obj*);
|
||||
obj* l_lean_position_decidable__lt___main(obj*, obj*);
|
||||
obj* l_state__t_monad___rarg(obj*);
|
||||
obj* l_lean_trace_trace__t_run___rarg(obj*, obj*, obj*);
|
||||
|
|
@ -181,14 +180,15 @@ return x_2;
|
|||
obj* l_lean_trace_trace___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
|
||||
_start:
|
||||
{
|
||||
obj* x_4; obj* x_7; obj* x_8;
|
||||
obj* x_4; obj* x_7; obj* x_8; obj* x_9;
|
||||
x_4 = lean::cnstr_get(x_1, 1);
|
||||
lean::inc(x_4);
|
||||
lean::dec(x_1);
|
||||
x_7 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_trace___rarg___lambda__1___boxed), 2, 1);
|
||||
lean::closure_set(x_7, 0, x_0);
|
||||
x_8 = lean::apply_4(x_4, lean::box(0), x_2, x_3, x_7);
|
||||
return x_8;
|
||||
x_8 = lean::mk_thunk(x_7);
|
||||
x_9 = lean::apply_4(x_4, lean::box(0), x_2, x_3, x_8);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
obj* l_lean_trace_trace___rarg___lambda__1(obj* x_0, unsigned char x_1) {
|
||||
|
|
@ -321,20 +321,21 @@ return x_29;
|
|||
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
|
||||
_start:
|
||||
{
|
||||
obj* x_6; obj* x_9; obj* x_10; obj* x_12; obj* x_13;
|
||||
obj* x_6; obj* x_9; obj* x_11; obj* x_13; obj* x_14;
|
||||
x_6 = lean::cnstr_get(x_5, 1);
|
||||
lean::inc(x_6);
|
||||
lean::dec(x_5);
|
||||
x_9 = l_thunk_get___rarg(x_0);
|
||||
x_10 = lean::apply_1(x_9, x_6);
|
||||
x_9 = lean::thunk_get(x_0);
|
||||
lean::dec(x_0);
|
||||
x_11 = lean::apply_1(x_9, x_6);
|
||||
lean::inc(x_4);
|
||||
x_12 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__2), 5, 4);
|
||||
lean::closure_set(x_12, 0, x_1);
|
||||
lean::closure_set(x_12, 1, x_2);
|
||||
lean::closure_set(x_12, 2, x_3);
|
||||
lean::closure_set(x_12, 3, x_4);
|
||||
x_13 = lean::apply_4(x_4, lean::box(0), lean::box(0), x_10, x_12);
|
||||
return x_13;
|
||||
x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__2), 5, 4);
|
||||
lean::closure_set(x_13, 0, x_1);
|
||||
lean::closure_set(x_13, 1, x_2);
|
||||
lean::closure_set(x_13, 2, x_3);
|
||||
lean::closure_set(x_13, 3, x_4);
|
||||
x_14 = lean::apply_4(x_4, lean::box(0), lean::box(0), x_11, x_13);
|
||||
return x_14;
|
||||
}
|
||||
}
|
||||
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__4(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
|
|
@ -359,83 +360,85 @@ lean::dec(x_7);
|
|||
x_17 = l_lean_kvmap_get__bool(x_14, x_5);
|
||||
if (lean::obj_tag(x_17) == 0)
|
||||
{
|
||||
obj* x_24; obj* x_25;
|
||||
obj* x_24; obj* x_26;
|
||||
lean::dec(x_11);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_3);
|
||||
lean::dec(x_17);
|
||||
x_24 = l_thunk_get___rarg(x_2);
|
||||
x_25 = lean::apply_1(x_24, x_9);
|
||||
return x_25;
|
||||
x_24 = lean::thunk_get(x_2);
|
||||
lean::dec(x_2);
|
||||
x_26 = lean::apply_1(x_24, x_9);
|
||||
return x_26;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_26; unsigned char x_29;
|
||||
x_26 = lean::cnstr_get(x_17, 0);
|
||||
lean::inc(x_26);
|
||||
obj* x_27; unsigned char x_30;
|
||||
x_27 = lean::cnstr_get(x_17, 0);
|
||||
lean::inc(x_27);
|
||||
lean::dec(x_17);
|
||||
x_29 = lean::unbox(x_26);
|
||||
lean::dec(x_26);
|
||||
if (x_29 == 0)
|
||||
x_30 = lean::unbox(x_27);
|
||||
lean::dec(x_27);
|
||||
if (x_30 == 0)
|
||||
{
|
||||
obj* x_36; obj* x_37;
|
||||
obj* x_37; obj* x_39;
|
||||
lean::dec(x_11);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_0);
|
||||
lean::dec(x_1);
|
||||
lean::dec(x_3);
|
||||
x_36 = l_thunk_get___rarg(x_2);
|
||||
x_37 = lean::apply_1(x_36, x_9);
|
||||
return x_37;
|
||||
x_37 = lean::thunk_get(x_2);
|
||||
lean::dec(x_2);
|
||||
x_39 = lean::apply_1(x_37, x_9);
|
||||
return x_39;
|
||||
}
|
||||
else
|
||||
{
|
||||
unsigned char x_38;
|
||||
x_38 = 0;
|
||||
x_12 = x_38;
|
||||
unsigned char x_40;
|
||||
x_40 = 0;
|
||||
x_12 = x_40;
|
||||
goto lbl_13;
|
||||
}
|
||||
}
|
||||
lbl_13:
|
||||
{
|
||||
obj* x_39; obj* x_41; obj* x_45; obj* x_46; obj* x_47; unsigned char x_48; obj* x_49; obj* x_50; obj* x_52; obj* x_54; obj* x_55;
|
||||
x_39 = lean::cnstr_get(x_9, 0);
|
||||
lean::inc(x_39);
|
||||
x_41 = lean::cnstr_get(x_9, 1);
|
||||
obj* x_41; obj* x_43; obj* x_47; obj* x_48; obj* x_49; unsigned char x_50; obj* x_51; obj* x_52; obj* x_54; obj* x_56; obj* x_57;
|
||||
x_41 = lean::cnstr_get(x_9, 0);
|
||||
lean::inc(x_41);
|
||||
x_43 = lean::cnstr_get(x_9, 1);
|
||||
lean::inc(x_43);
|
||||
lean::dec(x_9);
|
||||
lean::inc(x_0);
|
||||
x_45 = lean::alloc_cnstr(1, 1, 0);
|
||||
lean::cnstr_set(x_45, 0, x_0);
|
||||
x_46 = lean::alloc_cnstr(0, 0, 0);
|
||||
x_47 = lean::alloc_cnstr(1, 1, 0);
|
||||
lean::cnstr_set(x_47, 0, x_0);
|
||||
x_48 = lean::alloc_cnstr(0, 0, 0);
|
||||
;
|
||||
x_47 = lean::alloc_cnstr(0, 4, 0);
|
||||
lean::cnstr_set(x_47, 0, x_39);
|
||||
lean::cnstr_set(x_47, 1, x_41);
|
||||
lean::cnstr_set(x_47, 2, x_45);
|
||||
lean::cnstr_set(x_47, 3, x_46);
|
||||
x_48 = 0;
|
||||
x_49 = lean::box(x_48);
|
||||
x_49 = lean::alloc_cnstr(0, 4, 0);
|
||||
lean::cnstr_set(x_49, 0, x_41);
|
||||
lean::cnstr_set(x_49, 1, x_43);
|
||||
lean::cnstr_set(x_49, 2, x_47);
|
||||
lean::cnstr_set(x_49, 3, x_48);
|
||||
x_50 = 0;
|
||||
x_51 = lean::box(x_50);
|
||||
if (lean::is_scalar(x_11)) {
|
||||
x_50 = lean::alloc_cnstr(0, 2, 0);
|
||||
x_52 = lean::alloc_cnstr(0, 2, 0);
|
||||
} else {
|
||||
x_50 = x_11;
|
||||
x_52 = x_11;
|
||||
}
|
||||
lean::cnstr_set(x_50, 0, x_49);
|
||||
lean::cnstr_set(x_50, 1, x_47);
|
||||
lean::cnstr_set(x_52, 0, x_51);
|
||||
lean::cnstr_set(x_52, 1, x_49);
|
||||
lean::inc(x_1);
|
||||
x_52 = lean::apply_2(x_1, lean::box(0), x_50);
|
||||
x_54 = lean::apply_2(x_1, lean::box(0), x_52);
|
||||
lean::inc(x_4);
|
||||
x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__3), 6, 5);
|
||||
lean::closure_set(x_54, 0, x_2);
|
||||
lean::closure_set(x_54, 1, x_3);
|
||||
lean::closure_set(x_54, 2, x_0);
|
||||
lean::closure_set(x_54, 3, x_1);
|
||||
lean::closure_set(x_54, 4, x_4);
|
||||
x_55 = lean::apply_4(x_4, lean::box(0), lean::box(0), x_52, x_54);
|
||||
return x_55;
|
||||
x_56 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__3), 6, 5);
|
||||
lean::closure_set(x_56, 0, x_2);
|
||||
lean::closure_set(x_56, 1, x_3);
|
||||
lean::closure_set(x_56, 2, x_0);
|
||||
lean::closure_set(x_56, 3, x_1);
|
||||
lean::closure_set(x_56, 4, x_4);
|
||||
x_57 = lean::apply_4(x_4, lean::box(0), lean::box(0), x_54, x_56);
|
||||
return x_57;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -570,21 +573,22 @@ return x_33;
|
|||
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__9(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
|
||||
_start:
|
||||
{
|
||||
obj* x_7; obj* x_10; obj* x_11; obj* x_13; obj* x_14;
|
||||
obj* x_7; obj* x_10; obj* x_12; obj* x_14; obj* x_15;
|
||||
x_7 = lean::cnstr_get(x_6, 1);
|
||||
lean::inc(x_7);
|
||||
lean::dec(x_6);
|
||||
x_10 = l_thunk_get___rarg(x_0);
|
||||
x_11 = lean::apply_1(x_10, x_7);
|
||||
x_10 = lean::thunk_get(x_0);
|
||||
lean::dec(x_0);
|
||||
x_12 = lean::apply_1(x_10, x_7);
|
||||
lean::inc(x_5);
|
||||
x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__8), 6, 5);
|
||||
lean::closure_set(x_13, 0, x_1);
|
||||
lean::closure_set(x_13, 1, x_2);
|
||||
lean::closure_set(x_13, 2, x_3);
|
||||
lean::closure_set(x_13, 3, x_4);
|
||||
lean::closure_set(x_13, 4, x_5);
|
||||
x_14 = lean::apply_4(x_5, lean::box(0), lean::box(0), x_11, x_13);
|
||||
return x_14;
|
||||
x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__8), 6, 5);
|
||||
lean::closure_set(x_14, 0, x_1);
|
||||
lean::closure_set(x_14, 1, x_2);
|
||||
lean::closure_set(x_14, 2, x_3);
|
||||
lean::closure_set(x_14, 3, x_4);
|
||||
lean::closure_set(x_14, 4, x_5);
|
||||
x_15 = lean::apply_4(x_5, lean::box(0), lean::box(0), x_12, x_14);
|
||||
return x_15;
|
||||
}
|
||||
}
|
||||
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__10(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
|
||||
|
|
@ -605,7 +609,7 @@ if (lean::is_shared(x_8)) {
|
|||
}
|
||||
if (lean::obj_tag(x_9) == 0)
|
||||
{
|
||||
obj* x_23; obj* x_24;
|
||||
obj* x_23; obj* x_25;
|
||||
lean::dec(x_9);
|
||||
lean::dec(x_13);
|
||||
lean::dec(x_4);
|
||||
|
|
@ -615,105 +619,107 @@ lean::dec(x_7);
|
|||
lean::dec(x_1);
|
||||
lean::dec(x_2);
|
||||
lean::dec(x_3);
|
||||
x_23 = l_thunk_get___rarg(x_0);
|
||||
x_24 = lean::apply_1(x_23, x_11);
|
||||
return x_24;
|
||||
x_23 = lean::thunk_get(x_0);
|
||||
lean::dec(x_0);
|
||||
x_25 = lean::apply_1(x_23, x_11);
|
||||
return x_25;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_26; unsigned char x_28; unsigned char x_30; obj* x_33;
|
||||
obj* x_27; unsigned char x_29; unsigned char x_31; obj* x_34;
|
||||
lean::dec(x_9);
|
||||
x_26 = lean::cnstr_get(x_1, 0);
|
||||
lean::inc(x_26);
|
||||
lean::inc(x_26);
|
||||
x_33 = l_lean_kvmap_get__bool(x_26, x_7);
|
||||
if (lean::obj_tag(x_33) == 0)
|
||||
x_27 = lean::cnstr_get(x_1, 0);
|
||||
lean::inc(x_27);
|
||||
lean::inc(x_27);
|
||||
x_34 = l_lean_kvmap_get__bool(x_27, x_7);
|
||||
if (lean::obj_tag(x_34) == 0)
|
||||
{
|
||||
unsigned char x_39;
|
||||
unsigned char x_40;
|
||||
lean::dec(x_13);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
lean::dec(x_6);
|
||||
lean::dec(x_33);
|
||||
x_39 = 0;
|
||||
x_28 = x_39;
|
||||
goto lbl_29;
|
||||
lean::dec(x_34);
|
||||
x_40 = 0;
|
||||
x_29 = x_40;
|
||||
goto lbl_30;
|
||||
}
|
||||
else
|
||||
{
|
||||
obj* x_40; unsigned char x_43;
|
||||
x_40 = lean::cnstr_get(x_33, 0);
|
||||
lean::inc(x_40);
|
||||
lean::dec(x_33);
|
||||
x_43 = lean::unbox(x_40);
|
||||
lean::dec(x_40);
|
||||
if (x_43 == 0)
|
||||
obj* x_41; unsigned char x_44;
|
||||
x_41 = lean::cnstr_get(x_34, 0);
|
||||
lean::inc(x_41);
|
||||
lean::dec(x_34);
|
||||
x_44 = lean::unbox(x_41);
|
||||
lean::dec(x_41);
|
||||
if (x_44 == 0)
|
||||
{
|
||||
unsigned char x_49;
|
||||
unsigned char x_50;
|
||||
lean::dec(x_13);
|
||||
lean::dec(x_4);
|
||||
lean::dec(x_5);
|
||||
lean::dec(x_6);
|
||||
x_49 = 0;
|
||||
x_28 = x_49;
|
||||
goto lbl_29;
|
||||
x_50 = 0;
|
||||
x_29 = x_50;
|
||||
goto lbl_30;
|
||||
}
|
||||
else
|
||||
{
|
||||
unsigned char x_52;
|
||||
unsigned char x_53;
|
||||
lean::dec(x_11);
|
||||
lean::dec(x_3);
|
||||
x_52 = 0;
|
||||
x_30 = x_52;
|
||||
goto lbl_31;
|
||||
x_53 = 0;
|
||||
x_31 = x_53;
|
||||
goto lbl_32;
|
||||
}
|
||||
}
|
||||
lbl_29:
|
||||
lbl_30:
|
||||
{
|
||||
obj* x_53; obj* x_54; obj* x_55; obj* x_56;
|
||||
x_53 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__6), 3, 2);
|
||||
lean::closure_set(x_53, 0, x_1);
|
||||
lean::closure_set(x_53, 1, x_26);
|
||||
x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__7), 2, 1);
|
||||
lean::closure_set(x_54, 0, x_2);
|
||||
x_55 = l_thunk_get___rarg(x_0);
|
||||
x_56 = l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_3, lean::box(0), x_53, x_54, x_55, x_11);
|
||||
return x_56;
|
||||
obj* x_54; obj* x_55; obj* x_56; obj* x_58;
|
||||
x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__6), 3, 2);
|
||||
lean::closure_set(x_54, 0, x_1);
|
||||
lean::closure_set(x_54, 1, x_27);
|
||||
x_55 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__7), 2, 1);
|
||||
lean::closure_set(x_55, 0, x_2);
|
||||
x_56 = lean::thunk_get(x_0);
|
||||
lean::dec(x_0);
|
||||
x_58 = l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_3, lean::box(0), x_54, x_55, x_56, x_11);
|
||||
return x_58;
|
||||
}
|
||||
lbl_31:
|
||||
lbl_32:
|
||||
{
|
||||
obj* x_57; obj* x_59; obj* x_61; unsigned char x_62; obj* x_63; obj* x_64; obj* x_66; obj* x_68; obj* x_69;
|
||||
x_57 = lean::cnstr_get(x_1, 1);
|
||||
lean::inc(x_57);
|
||||
x_59 = lean::alloc_cnstr(0, 0, 0);
|
||||
;
|
||||
obj* x_59; obj* x_61; obj* x_63; unsigned char x_64; obj* x_65; obj* x_66; obj* x_68; obj* x_70; obj* x_71;
|
||||
x_59 = lean::cnstr_get(x_1, 1);
|
||||
lean::inc(x_59);
|
||||
x_61 = lean::alloc_cnstr(0, 4, 0);
|
||||
lean::cnstr_set(x_61, 0, x_26);
|
||||
lean::cnstr_set(x_61, 1, x_57);
|
||||
lean::cnstr_set(x_61, 2, x_2);
|
||||
lean::cnstr_set(x_61, 3, x_59);
|
||||
x_62 = 0;
|
||||
x_63 = lean::box(x_62);
|
||||
x_61 = lean::alloc_cnstr(0, 0, 0);
|
||||
;
|
||||
lean::inc(x_61);
|
||||
x_63 = lean::alloc_cnstr(0, 4, 0);
|
||||
lean::cnstr_set(x_63, 0, x_27);
|
||||
lean::cnstr_set(x_63, 1, x_59);
|
||||
lean::cnstr_set(x_63, 2, x_2);
|
||||
lean::cnstr_set(x_63, 3, x_61);
|
||||
x_64 = 0;
|
||||
x_65 = lean::box(x_64);
|
||||
if (lean::is_scalar(x_13)) {
|
||||
x_64 = lean::alloc_cnstr(0, 2, 0);
|
||||
x_66 = lean::alloc_cnstr(0, 2, 0);
|
||||
} else {
|
||||
x_64 = x_13;
|
||||
x_66 = x_13;
|
||||
}
|
||||
lean::cnstr_set(x_64, 0, x_63);
|
||||
lean::cnstr_set(x_64, 1, x_61);
|
||||
lean::cnstr_set(x_66, 0, x_65);
|
||||
lean::cnstr_set(x_66, 1, x_63);
|
||||
lean::inc(x_4);
|
||||
x_66 = lean::apply_2(x_4, lean::box(0), x_64);
|
||||
x_68 = lean::apply_2(x_4, lean::box(0), x_66);
|
||||
lean::inc(x_6);
|
||||
x_68 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__9), 7, 6);
|
||||
lean::closure_set(x_68, 0, x_0);
|
||||
lean::closure_set(x_68, 1, x_1);
|
||||
lean::closure_set(x_68, 2, x_5);
|
||||
lean::closure_set(x_68, 3, x_59);
|
||||
lean::closure_set(x_68, 4, x_4);
|
||||
lean::closure_set(x_68, 5, x_6);
|
||||
x_69 = lean::apply_4(x_6, lean::box(0), lean::box(0), x_66, x_68);
|
||||
return x_69;
|
||||
x_70 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__9), 7, 6);
|
||||
lean::closure_set(x_70, 0, x_0);
|
||||
lean::closure_set(x_70, 1, x_1);
|
||||
lean::closure_set(x_70, 2, x_5);
|
||||
lean::closure_set(x_70, 3, x_61);
|
||||
lean::closure_set(x_70, 4, x_4);
|
||||
lean::closure_set(x_70, 5, x_6);
|
||||
x_71 = lean::apply_4(x_6, lean::box(0), lean::box(0), x_68, x_70);
|
||||
return x_71;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ obj* _init_l_lean_githash() {
|
|||
_start:
|
||||
{
|
||||
obj* x_0;
|
||||
x_0 = lean::mk_string("4d668362551df18e7f1949f65c281a7d865dc97a");
|
||||
x_0 = lean::mk_string("7c355d3ba60e86b89fc9da89ee7ea2cfd24c3cf3");
|
||||
return x_0;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue