max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Lean stage0 autoupdater 2024-02-19 15:51:18 +00:00
parent 1d66c32d5f
commit 7545b85512
17 changed files with 10941 additions and 5686 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1295
stage0/stdlib/Init/Tactics.c generated
View file

File diff suppressed because it is too large Load diff

1008
stage0/stdlib/Lean/Compiler/LCNF/Main.c generated
View file

File diff suppressed because it is too large Load diff

2298
stage0/stdlib/Lean/Elab/Command.c generated
View file

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean/Elab/Tactic.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Tactic
// Imports: Lean.Elab.Term Lean.Elab.Tactic.Basic Lean.Elab.Tactic.ElabTerm Lean.Elab.Tactic.Induction Lean.Elab.Tactic.Generalize Lean.Elab.Tactic.Injection Lean.Elab.Tactic.Match Lean.Elab.Tactic.Rewrite Lean.Elab.Tactic.Location Lean.Elab.Tactic.Simp Lean.Elab.Tactic.Simproc Lean.Elab.Tactic.BuiltinTactic Lean.Elab.Tactic.Split Lean.Elab.Tactic.Conv Lean.Elab.Tactic.Delta Lean.Elab.Tactic.Meta Lean.Elab.Tactic.Unfold Lean.Elab.Tactic.Cache Lean.Elab.Tactic.Calc Lean.Elab.Tactic.Congr Lean.Elab.Tactic.Guard Lean.Elab.Tactic.RCases Lean.Elab.Tactic.Repeat Lean.Elab.Tactic.Ext Lean.Elab.Tactic.Change Lean.Elab.Tactic.FalseOrByContra Lean.Elab.Tactic.Omega
// Imports: Lean.Elab.Term Lean.Elab.Tactic.Basic Lean.Elab.Tactic.ElabTerm Lean.Elab.Tactic.Induction Lean.Elab.Tactic.Generalize Lean.Elab.Tactic.Injection Lean.Elab.Tactic.Match Lean.Elab.Tactic.Rewrite Lean.Elab.Tactic.Location Lean.Elab.Tactic.Simp Lean.Elab.Tactic.Simproc Lean.Elab.Tactic.BuiltinTactic Lean.Elab.Tactic.Split Lean.Elab.Tactic.Conv Lean.Elab.Tactic.Delta Lean.Elab.Tactic.Meta Lean.Elab.Tactic.Unfold Lean.Elab.Tactic.Cache Lean.Elab.Tactic.Calc Lean.Elab.Tactic.Congr Lean.Elab.Tactic.Guard Lean.Elab.Tactic.RCases Lean.Elab.Tactic.Repeat Lean.Elab.Tactic.Ext Lean.Elab.Tactic.Change Lean.Elab.Tactic.FalseOrByContra Lean.Elab.Tactic.Omega Lean.Elab.Tactic.Simpa
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -40,6 +40,7 @@ lean_object* initialize_Lean_Elab_Tactic_Ext(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Change(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_FalseOrByContra(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Omega(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Tactic_Simpa(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Elab_Tactic(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -126,6 +127,9 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Omega(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Simpa(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

205
stage0/stdlib/Lean/Elab/Tactic/Basic.c generated
View file

@ -7048,12 +7048,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic__
_start:
{
lean_object* x_11;
lean_inc(x_8);
x_11 = lean_apply_9(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_11) == 0)
{
uint8_t x_12;
lean_dec(x_8);
x_12 = !lean_is_exclusive(x_11);
if (x_12 == 0)
{
@ -7086,83 +7084,28 @@ uint8_t x_19;
x_19 = !lean_is_exclusive(x_11);
if (x_19 == 0)
{
lean_object* x_20; uint8_t x_21;
lean_object* x_20; lean_object* x_21;
x_20 = lean_ctor_get(x_11, 0);
x_21 = l_Lean_Exception_isRuntime(x_20);
if (x_21 == 0)
{
lean_object* x_22;
lean_dec(x_8);
x_22 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_22, 0, x_20);
x_21 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set_tag(x_11, 0);
lean_ctor_set(x_11, 0, x_22);
lean_ctor_set(x_11, 0, x_21);
return x_11;
}
else
{
uint8_t x_23;
x_23 = lean_ctor_get_uint8(x_8, sizeof(void*)*11);
lean_dec(x_8);
if (x_23 == 0)
{
return x_11;
}
else
{
lean_object* x_24;
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_20);
lean_ctor_set_tag(x_11, 0);
lean_ctor_set(x_11, 0, x_24);
return x_11;
}
}
}
else
{
lean_object* x_25; lean_object* x_26; uint8_t x_27;
x_25 = lean_ctor_get(x_11, 0);
x_26 = lean_ctor_get(x_11, 1);
lean_inc(x_26);
lean_inc(x_25);
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_11, 0);
x_23 = lean_ctor_get(x_11, 1);
lean_inc(x_23);
lean_inc(x_22);
lean_dec(x_11);
x_27 = l_Lean_Exception_isRuntime(x_25);
if (x_27 == 0)
{
lean_object* x_28; lean_object* x_29;
lean_dec(x_8);
x_28 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_28, 0, x_25);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_26);
return x_29;
}
else
{
uint8_t x_30;
x_30 = lean_ctor_get_uint8(x_8, sizeof(void*)*11);
lean_dec(x_8);
if (x_30 == 0)
{
lean_object* x_31;
x_31 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_31, 0, x_25);
lean_ctor_set(x_31, 1, x_26);
return x_31;
}
else
{
lean_object* x_32; lean_object* x_33;
x_32 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_32, 0, x_25);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_26);
return x_33;
}
}
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_22);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_23);
return x_25;
}
}
}
@ -7355,123 +7298,17 @@ return x_24;
}
else
{
uint8_t x_25;
x_25 = !lean_is_exclusive(x_21);
if (x_25 == 0)
{
lean_object* x_26; lean_object* x_27; uint8_t x_28;
x_26 = lean_ctor_get(x_21, 0);
x_27 = lean_ctor_get(x_21, 1);
x_28 = l_Lean_Exception_isRuntime(x_26);
if (x_28 == 0)
{
lean_object* x_29; lean_object* x_30;
lean_free_object(x_21);
lean_dec(x_26);
x_29 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3___lambda__4___closed__2;
x_30 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3___lambda__3(x_1, x_2, x_20, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_29, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_18, x_27);
lean_dec(x_18);
lean_dec(x_15);
lean_dec(x_12);
lean_dec(x_4);
return x_30;
}
else
{
uint8_t x_31;
x_31 = lean_ctor_get_uint8(x_17, sizeof(void*)*11);
if (x_31 == 0)
{
lean_dec(x_20);
lean_dec(x_18);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_21;
}
else
{
lean_object* x_32; lean_object* x_33;
lean_free_object(x_21);
lean_dec(x_26);
x_32 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3___lambda__4___closed__2;
x_33 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3___lambda__3(x_1, x_2, x_20, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_32, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_18, x_27);
lean_dec(x_18);
lean_dec(x_15);
lean_dec(x_12);
lean_dec(x_4);
return x_33;
}
}
}
else
{
lean_object* x_34; lean_object* x_35; uint8_t x_36;
x_34 = lean_ctor_get(x_21, 0);
x_35 = lean_ctor_get(x_21, 1);
lean_inc(x_35);
lean_inc(x_34);
lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_25 = lean_ctor_get(x_21, 1);
lean_inc(x_25);
lean_dec(x_21);
x_36 = l_Lean_Exception_isRuntime(x_34);
if (x_36 == 0)
{
lean_object* x_37; lean_object* x_38;
lean_dec(x_34);
x_37 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3___lambda__4___closed__2;
x_38 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3___lambda__3(x_1, x_2, x_20, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_37, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_18, x_35);
x_26 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3___lambda__4___closed__2;
x_27 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3___lambda__3(x_1, x_2, x_20, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_26, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_18, x_25);
lean_dec(x_18);
lean_dec(x_15);
lean_dec(x_12);
lean_dec(x_4);
return x_38;
}
else
{
uint8_t x_39;
x_39 = lean_ctor_get_uint8(x_17, sizeof(void*)*11);
if (x_39 == 0)
{
lean_object* x_40;
lean_dec(x_20);
lean_dec(x_18);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_34);
lean_ctor_set(x_40, 1, x_35);
return x_40;
}
else
{
lean_object* x_41; lean_object* x_42;
lean_dec(x_34);
x_41 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3___lambda__4___closed__2;
x_42 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3___lambda__3(x_1, x_2, x_20, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_41, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_18, x_35);
lean_dec(x_18);
lean_dec(x_15);
lean_dec(x_12);
lean_dec(x_4);
return x_42;
}
}
}
return x_27;
}
}
}

5340
stage0/stdlib/Lean/Elab/Tactic/Simpa.c generated Normal file
View file

File diff suppressed because it is too large Load diff

198
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -27144,12 +27144,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__
_start:
{
lean_object* x_9;
lean_inc(x_6);
x_9 = lean_apply_7(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
if (lean_obj_tag(x_9) == 0)
{
uint8_t x_10;
lean_dec(x_6);
x_10 = !lean_is_exclusive(x_9);
if (x_10 == 0)
{
@ -27182,83 +27180,28 @@ uint8_t x_17;
x_17 = !lean_is_exclusive(x_9);
if (x_17 == 0)
{
lean_object* x_18; uint8_t x_19;
lean_object* x_18; lean_object* x_19;
x_18 = lean_ctor_get(x_9, 0);
x_19 = l_Lean_Exception_isRuntime(x_18);
if (x_19 == 0)
{
lean_object* x_20;
lean_dec(x_6);
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_18);
x_19 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set_tag(x_9, 0);
lean_ctor_set(x_9, 0, x_20);
lean_ctor_set(x_9, 0, x_19);
return x_9;
}
else
{
uint8_t x_21;
x_21 = lean_ctor_get_uint8(x_6, sizeof(void*)*11);
lean_dec(x_6);
if (x_21 == 0)
{
return x_9;
}
else
{
lean_object* x_22;
x_22 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_22, 0, x_18);
lean_ctor_set_tag(x_9, 0);
lean_ctor_set(x_9, 0, x_22);
return x_9;
}
}
}
else
{
lean_object* x_23; lean_object* x_24; uint8_t x_25;
x_23 = lean_ctor_get(x_9, 0);
x_24 = lean_ctor_get(x_9, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_20 = lean_ctor_get(x_9, 0);
x_21 = lean_ctor_get(x_9, 1);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_9);
x_25 = l_Lean_Exception_isRuntime(x_23);
if (x_25 == 0)
{
lean_object* x_26; lean_object* x_27;
lean_dec(x_6);
x_26 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_26, 0, x_23);
x_27 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_24);
return x_27;
}
else
{
uint8_t x_28;
x_28 = lean_ctor_get_uint8(x_6, sizeof(void*)*11);
lean_dec(x_6);
if (x_28 == 0)
{
lean_object* x_29;
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_23);
lean_ctor_set(x_29, 1, x_24);
return x_29;
}
else
{
lean_object* x_30; lean_object* x_31;
x_30 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_30, 0, x_23);
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_24);
return x_31;
}
}
x_22 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_22, 0, x_20);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
return x_23;
}
}
}
@ -27447,115 +27390,16 @@ return x_22;
}
else
{
uint8_t x_23;
x_23 = !lean_is_exclusive(x_19);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_19, 0);
x_25 = lean_ctor_get(x_19, 1);
x_26 = l_Lean_Exception_isRuntime(x_24);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
lean_free_object(x_19);
lean_dec(x_24);
x_27 = l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__1___lambda__4___closed__2;
x_28 = l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__1___lambda__3(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_27, x_11, x_12, x_13, x_14, x_15, x_16, x_25);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_28;
}
else
{
uint8_t x_29;
x_29 = lean_ctor_get_uint8(x_15, sizeof(void*)*11);
if (x_29 == 0)
{
lean_dec(x_18);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_19;
}
else
{
lean_object* x_30; lean_object* x_31;
lean_free_object(x_19);
lean_dec(x_24);
x_30 = l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__1___lambda__4___closed__2;
x_31 = l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__1___lambda__3(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_30, x_11, x_12, x_13, x_14, x_15, x_16, x_25);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_31;
}
}
}
else
{
lean_object* x_32; lean_object* x_33; uint8_t x_34;
x_32 = lean_ctor_get(x_19, 0);
x_33 = lean_ctor_get(x_19, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_19, 1);
lean_inc(x_23);
lean_dec(x_19);
x_34 = l_Lean_Exception_isRuntime(x_32);
if (x_34 == 0)
{
lean_object* x_35; lean_object* x_36;
lean_dec(x_32);
x_35 = l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__1___lambda__4___closed__2;
x_36 = l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__1___lambda__3(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_35, x_11, x_12, x_13, x_14, x_15, x_16, x_33);
x_24 = l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__1___lambda__4___closed__2;
x_25 = l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__1___lambda__3(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_24, x_11, x_12, x_13, x_14, x_15, x_16, x_23);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_36;
}
else
{
uint8_t x_37;
x_37 = lean_ctor_get_uint8(x_15, sizeof(void*)*11);
if (x_37 == 0)
{
lean_object* x_38;
lean_dec(x_18);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_32);
lean_ctor_set(x_38, 1, x_33);
return x_38;
}
else
{
lean_object* x_39; lean_object* x_40;
lean_dec(x_32);
x_39 = l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__1___lambda__4___closed__2;
x_40 = l_Lean_withTraceNode___at_Lean_Elab_Term_mkCoe___spec__1___lambda__3(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_39, x_11, x_12, x_13, x_14, x_15, x_16, x_33);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_40;
}
}
}
return x_25;
}
}
}

194
stage0/stdlib/Lean/Meta/AppBuilder.c generated
View file

@ -9231,12 +9231,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilde
_start:
{
lean_object* x_7;
lean_inc(x_4);
x_7 = lean_apply_5(x_1, x_2, x_3, x_4, x_5, x_6);
if (lean_obj_tag(x_7) == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
@ -9269,83 +9267,28 @@ uint8_t x_15;
x_15 = !lean_is_exclusive(x_7);
if (x_15 == 0)
{
lean_object* x_16; uint8_t x_17;
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_7, 0);
x_17 = l_Lean_Exception_isRuntime(x_16);
if (x_17 == 0)
{
lean_object* x_18;
lean_dec(x_4);
x_18 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_18, 0, x_16);
x_17 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_18);
lean_ctor_set(x_7, 0, x_17);
return x_7;
}
else
{
uint8_t x_19;
x_19 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_19 == 0)
{
return x_7;
}
else
{
lean_object* x_20;
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_20);
return x_7;
}
}
}
else
{
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_7, 0);
x_22 = lean_ctor_get(x_7, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_7, 0);
x_19 = lean_ctor_get(x_7, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_7);
x_23 = l_Lean_Exception_isRuntime(x_21);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25;
lean_dec(x_4);
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_21);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_22);
return x_25;
}
else
{
uint8_t x_26;
x_26 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_26 == 0)
{
lean_object* x_27;
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_21);
lean_ctor_set(x_27, 1, x_22);
return x_27;
}
else
{
lean_object* x_28; lean_object* x_29;
x_28 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_28, 0, x_21);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_22);
return x_29;
}
}
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_18);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
}
@ -9528,111 +9471,16 @@ return x_20;
}
else
{
uint8_t x_21;
x_21 = !lean_is_exclusive(x_17);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_22 = lean_ctor_get(x_17, 0);
x_23 = lean_ctor_get(x_17, 1);
x_24 = l_Lean_Exception_isRuntime(x_22);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26;
lean_free_object(x_17);
lean_dec(x_22);
x_25 = l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_withAppBuilderTrace___spec__1___lambda__4___closed__2;
x_26 = l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_withAppBuilderTrace___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_25, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_26;
}
else
{
uint8_t x_27;
x_27 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_27 == 0)
{
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_17;
}
else
{
lean_object* x_28; lean_object* x_29;
lean_free_object(x_17);
lean_dec(x_22);
x_28 = l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_withAppBuilderTrace___spec__1___lambda__4___closed__2;
x_29 = l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_withAppBuilderTrace___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_28, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_29;
}
}
}
else
{
lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_30 = lean_ctor_get(x_17, 0);
x_31 = lean_ctor_get(x_17, 1);
lean_inc(x_31);
lean_inc(x_30);
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 1);
lean_inc(x_21);
lean_dec(x_17);
x_32 = l_Lean_Exception_isRuntime(x_30);
if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34;
lean_dec(x_30);
x_33 = l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_withAppBuilderTrace___spec__1___lambda__4___closed__2;
x_34 = l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_withAppBuilderTrace___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_33, x_11, x_12, x_13, x_14, x_31);
x_22 = l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_withAppBuilderTrace___spec__1___lambda__4___closed__2;
x_23 = l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_withAppBuilderTrace___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_22, x_11, x_12, x_13, x_14, x_21);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_34;
}
else
{
uint8_t x_35;
x_35 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_35 == 0)
{
lean_object* x_36;
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_30);
lean_ctor_set(x_36, 1, x_31);
return x_36;
}
else
{
lean_object* x_37; lean_object* x_38;
lean_dec(x_30);
x_37 = l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_withAppBuilderTrace___spec__1___lambda__4___closed__2;
x_38 = l_Lean_withTraceNode___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_withAppBuilderTrace___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_37, x_11, x_12, x_13, x_14, x_31);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_38;
}
}
}
return x_23;
}
}
}

194
stage0/stdlib/Lean/Meta/Basic.c generated
View file

@ -34539,12 +34539,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Meta_processPostponed___
_start:
{
lean_object* x_7;
lean_inc(x_4);
x_7 = lean_apply_5(x_1, x_2, x_3, x_4, x_5, x_6);
if (lean_obj_tag(x_7) == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
@ -34577,83 +34575,28 @@ uint8_t x_15;
x_15 = !lean_is_exclusive(x_7);
if (x_15 == 0)
{
lean_object* x_16; uint8_t x_17;
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_7, 0);
x_17 = l_Lean_Exception_isRuntime(x_16);
if (x_17 == 0)
{
lean_object* x_18;
lean_dec(x_4);
x_18 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_18, 0, x_16);
x_17 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_18);
lean_ctor_set(x_7, 0, x_17);
return x_7;
}
else
{
uint8_t x_19;
x_19 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_19 == 0)
{
return x_7;
}
else
{
lean_object* x_20;
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_20);
return x_7;
}
}
}
else
{
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_7, 0);
x_22 = lean_ctor_get(x_7, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_7, 0);
x_19 = lean_ctor_get(x_7, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_7);
x_23 = l_Lean_Exception_isRuntime(x_21);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25;
lean_dec(x_4);
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_21);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_22);
return x_25;
}
else
{
uint8_t x_26;
x_26 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_26 == 0)
{
lean_object* x_27;
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_21);
lean_ctor_set(x_27, 1, x_22);
return x_27;
}
else
{
lean_object* x_28; lean_object* x_29;
x_28 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_28, 0, x_21);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_22);
return x_29;
}
}
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_18);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
}
@ -34836,111 +34779,16 @@ return x_20;
}
else
{
uint8_t x_21;
x_21 = !lean_is_exclusive(x_17);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_22 = lean_ctor_get(x_17, 0);
x_23 = lean_ctor_get(x_17, 1);
x_24 = l_Lean_Exception_isRuntime(x_22);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26;
lean_free_object(x_17);
lean_dec(x_22);
x_25 = l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__4___closed__2;
x_26 = l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_25, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_26;
}
else
{
uint8_t x_27;
x_27 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_27 == 0)
{
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_17;
}
else
{
lean_object* x_28; lean_object* x_29;
lean_free_object(x_17);
lean_dec(x_22);
x_28 = l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__4___closed__2;
x_29 = l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_28, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_29;
}
}
}
else
{
lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_30 = lean_ctor_get(x_17, 0);
x_31 = lean_ctor_get(x_17, 1);
lean_inc(x_31);
lean_inc(x_30);
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 1);
lean_inc(x_21);
lean_dec(x_17);
x_32 = l_Lean_Exception_isRuntime(x_30);
if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34;
lean_dec(x_30);
x_33 = l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__4___closed__2;
x_34 = l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_33, x_11, x_12, x_13, x_14, x_31);
x_22 = l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__4___closed__2;
x_23 = l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_22, x_11, x_12, x_13, x_14, x_21);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_34;
}
else
{
uint8_t x_35;
x_35 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_35 == 0)
{
lean_object* x_36;
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_30);
lean_ctor_set(x_36, 1, x_31);
return x_36;
}
else
{
lean_object* x_37; lean_object* x_38;
lean_dec(x_30);
x_37 = l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__4___closed__2;
x_38 = l_Lean_withTraceNode___at_Lean_Meta_processPostponed___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_37, x_11, x_12, x_13, x_14, x_31);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_38;
}
}
}
return x_23;
}
}
}

194
stage0/stdlib/Lean/Meta/Check.c generated
View file

@ -7839,12 +7839,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___l
_start:
{
lean_object* x_7;
lean_inc(x_4);
x_7 = lean_apply_5(x_1, x_2, x_3, x_4, x_5, x_6);
if (lean_obj_tag(x_7) == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
@ -7877,83 +7875,28 @@ uint8_t x_15;
x_15 = !lean_is_exclusive(x_7);
if (x_15 == 0)
{
lean_object* x_16; uint8_t x_17;
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_7, 0);
x_17 = l_Lean_Exception_isRuntime(x_16);
if (x_17 == 0)
{
lean_object* x_18;
lean_dec(x_4);
x_18 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_18, 0, x_16);
x_17 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_18);
lean_ctor_set(x_7, 0, x_17);
return x_7;
}
else
{
uint8_t x_19;
x_19 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_19 == 0)
{
return x_7;
}
else
{
lean_object* x_20;
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_20);
return x_7;
}
}
}
else
{
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_7, 0);
x_22 = lean_ctor_get(x_7, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_7, 0);
x_19 = lean_ctor_get(x_7, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_7);
x_23 = l_Lean_Exception_isRuntime(x_21);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25;
lean_dec(x_4);
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_21);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_22);
return x_25;
}
else
{
uint8_t x_26;
x_26 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_26 == 0)
{
lean_object* x_27;
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_21);
lean_ctor_set(x_27, 1, x_22);
return x_27;
}
else
{
lean_object* x_28; lean_object* x_29;
x_28 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_28, 0, x_21);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_22);
return x_29;
}
}
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_18);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
}
@ -8136,111 +8079,16 @@ return x_20;
}
else
{
uint8_t x_21;
x_21 = !lean_is_exclusive(x_17);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_22 = lean_ctor_get(x_17, 0);
x_23 = lean_ctor_get(x_17, 1);
x_24 = l_Lean_Exception_isRuntime(x_22);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26;
lean_free_object(x_17);
lean_dec(x_22);
x_25 = l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___lambda__4___closed__2;
x_26 = l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_25, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_26;
}
else
{
uint8_t x_27;
x_27 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_27 == 0)
{
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_17;
}
else
{
lean_object* x_28; lean_object* x_29;
lean_free_object(x_17);
lean_dec(x_22);
x_28 = l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___lambda__4___closed__2;
x_29 = l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_28, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_29;
}
}
}
else
{
lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_30 = lean_ctor_get(x_17, 0);
x_31 = lean_ctor_get(x_17, 1);
lean_inc(x_31);
lean_inc(x_30);
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 1);
lean_inc(x_21);
lean_dec(x_17);
x_32 = l_Lean_Exception_isRuntime(x_30);
if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34;
lean_dec(x_30);
x_33 = l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___lambda__4___closed__2;
x_34 = l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_33, x_11, x_12, x_13, x_14, x_31);
x_22 = l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___lambda__4___closed__2;
x_23 = l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_22, x_11, x_12, x_13, x_14, x_21);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_34;
}
else
{
uint8_t x_35;
x_35 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_35 == 0)
{
lean_object* x_36;
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_30);
lean_ctor_set(x_36, 1, x_31);
return x_36;
}
else
{
lean_object* x_37; lean_object* x_38;
lean_dec(x_30);
x_37 = l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___lambda__4___closed__2;
x_38 = l_Lean_withTraceNode___at_Lean_Meta_check___spec__1___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_37, x_11, x_12, x_13, x_14, x_31);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_38;
}
}
}
return x_23;
}
}
}

87
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

@ -11664,12 +11664,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNodeBefore___at___private_Lean_Meta_Exp
_start:
{
lean_object* x_7;
lean_inc(x_4);
x_7 = lean_apply_5(x_1, x_2, x_3, x_4, x_5, x_6);
if (lean_obj_tag(x_7) == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
@ -11702,83 +11700,28 @@ uint8_t x_15;
x_15 = !lean_is_exclusive(x_7);
if (x_15 == 0)
{
lean_object* x_16; uint8_t x_17;
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_7, 0);
x_17 = l_Lean_Exception_isRuntime(x_16);
if (x_17 == 0)
{
lean_object* x_18;
lean_dec(x_4);
x_18 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_18, 0, x_16);
x_17 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_18);
lean_ctor_set(x_7, 0, x_17);
return x_7;
}
else
{
uint8_t x_19;
x_19 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_19 == 0)
{
return x_7;
}
else
{
lean_object* x_20;
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_20);
return x_7;
}
}
}
else
{
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_7, 0);
x_22 = lean_ctor_get(x_7, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_7, 0);
x_19 = lean_ctor_get(x_7, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_7);
x_23 = l_Lean_Exception_isRuntime(x_21);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25;
lean_dec(x_4);
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_21);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_22);
return x_25;
}
else
{
uint8_t x_26;
x_26 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_26 == 0)
{
lean_object* x_27;
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_21);
lean_ctor_set(x_27, 1, x_22);
return x_27;
}
else
{
lean_object* x_28; lean_object* x_29;
x_28 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_28, 0, x_21);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_22);
return x_29;
}
}
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_18);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
}

194
stage0/stdlib/Lean/Meta/Injective.c generated
View file

@ -5027,12 +5027,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems
_start:
{
lean_object* x_7;
lean_inc(x_4);
x_7 = lean_apply_5(x_1, x_2, x_3, x_4, x_5, x_6);
if (lean_obj_tag(x_7) == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
@ -5065,83 +5063,28 @@ uint8_t x_15;
x_15 = !lean_is_exclusive(x_7);
if (x_15 == 0)
{
lean_object* x_16; uint8_t x_17;
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_7, 0);
x_17 = l_Lean_Exception_isRuntime(x_16);
if (x_17 == 0)
{
lean_object* x_18;
lean_dec(x_4);
x_18 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_18, 0, x_16);
x_17 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_18);
lean_ctor_set(x_7, 0, x_17);
return x_7;
}
else
{
uint8_t x_19;
x_19 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_19 == 0)
{
return x_7;
}
else
{
lean_object* x_20;
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_20);
return x_7;
}
}
}
else
{
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_7, 0);
x_22 = lean_ctor_get(x_7, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_7, 0);
x_19 = lean_ctor_get(x_7, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_7);
x_23 = l_Lean_Exception_isRuntime(x_21);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25;
lean_dec(x_4);
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_21);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_22);
return x_25;
}
else
{
uint8_t x_26;
x_26 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_26 == 0)
{
lean_object* x_27;
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_21);
lean_ctor_set(x_27, 1, x_22);
return x_27;
}
else
{
lean_object* x_28; lean_object* x_29;
x_28 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_28, 0, x_21);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_22);
return x_29;
}
}
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_18);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
}
@ -5324,111 +5267,16 @@ return x_20;
}
else
{
uint8_t x_21;
x_21 = !lean_is_exclusive(x_17);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_22 = lean_ctor_get(x_17, 0);
x_23 = lean_ctor_get(x_17, 1);
x_24 = l_Lean_Exception_isRuntime(x_22);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26;
lean_free_object(x_17);
lean_dec(x_22);
x_25 = l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems___spec__5___lambda__4___closed__2;
x_26 = l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems___spec__5___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_25, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_26;
}
else
{
uint8_t x_27;
x_27 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_27 == 0)
{
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_17;
}
else
{
lean_object* x_28; lean_object* x_29;
lean_free_object(x_17);
lean_dec(x_22);
x_28 = l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems___spec__5___lambda__4___closed__2;
x_29 = l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems___spec__5___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_28, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_29;
}
}
}
else
{
lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_30 = lean_ctor_get(x_17, 0);
x_31 = lean_ctor_get(x_17, 1);
lean_inc(x_31);
lean_inc(x_30);
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 1);
lean_inc(x_21);
lean_dec(x_17);
x_32 = l_Lean_Exception_isRuntime(x_30);
if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34;
lean_dec(x_30);
x_33 = l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems___spec__5___lambda__4___closed__2;
x_34 = l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems___spec__5___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_33, x_11, x_12, x_13, x_14, x_31);
x_22 = l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems___spec__5___lambda__4___closed__2;
x_23 = l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems___spec__5___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_22, x_11, x_12, x_13, x_14, x_21);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_34;
}
else
{
uint8_t x_35;
x_35 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_35 == 0)
{
lean_object* x_36;
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_30);
lean_ctor_set(x_36, 1, x_31);
return x_36;
}
else
{
lean_object* x_37; lean_object* x_38;
lean_dec(x_30);
x_37 = l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems___spec__5___lambda__4___closed__2;
x_38 = l_Lean_withTraceNode___at_Lean_Meta_mkInjectiveTheorems___spec__5___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_37, x_11, x_12, x_13, x_14, x_31);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_38;
}
}
}
return x_23;
}
}
}

721
stage0/stdlib/Lean/Meta/SynthInstance.c generated
View file

@ -6018,12 +6018,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSu
_start:
{
lean_object* x_9;
lean_inc(x_6);
x_9 = lean_apply_7(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
if (lean_obj_tag(x_9) == 0)
{
uint8_t x_10;
lean_dec(x_6);
x_10 = !lean_is_exclusive(x_9);
if (x_10 == 0)
{
@ -6056,83 +6054,28 @@ uint8_t x_17;
x_17 = !lean_is_exclusive(x_9);
if (x_17 == 0)
{
lean_object* x_18; uint8_t x_19;
lean_object* x_18; lean_object* x_19;
x_18 = lean_ctor_get(x_9, 0);
x_19 = l_Lean_Exception_isRuntime(x_18);
if (x_19 == 0)
{
lean_object* x_20;
lean_dec(x_6);
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_18);
x_19 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set_tag(x_9, 0);
lean_ctor_set(x_9, 0, x_20);
lean_ctor_set(x_9, 0, x_19);
return x_9;
}
else
{
uint8_t x_21;
x_21 = lean_ctor_get_uint8(x_6, sizeof(void*)*11);
lean_dec(x_6);
if (x_21 == 0)
{
return x_9;
}
else
{
lean_object* x_22;
x_22 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_22, 0, x_18);
lean_ctor_set_tag(x_9, 0);
lean_ctor_set(x_9, 0, x_22);
return x_9;
}
}
}
else
{
lean_object* x_23; lean_object* x_24; uint8_t x_25;
x_23 = lean_ctor_get(x_9, 0);
x_24 = lean_ctor_get(x_9, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_20 = lean_ctor_get(x_9, 0);
x_21 = lean_ctor_get(x_9, 1);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_9);
x_25 = l_Lean_Exception_isRuntime(x_23);
if (x_25 == 0)
{
lean_object* x_26; lean_object* x_27;
lean_dec(x_6);
x_26 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_26, 0, x_23);
x_27 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_24);
return x_27;
}
else
{
uint8_t x_28;
x_28 = lean_ctor_get_uint8(x_6, sizeof(void*)*11);
lean_dec(x_6);
if (x_28 == 0)
{
lean_object* x_29;
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_23);
lean_ctor_set(x_29, 1, x_24);
return x_29;
}
else
{
lean_object* x_30; lean_object* x_31;
x_30 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_30, 0, x_23);
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_24);
return x_31;
}
}
x_22 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_22, 0, x_20);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
return x_23;
}
}
}
@ -6321,115 +6264,16 @@ return x_22;
}
else
{
uint8_t x_23;
x_23 = !lean_is_exclusive(x_19);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_19, 0);
x_25 = lean_ctor_get(x_19, 1);
x_26 = l_Lean_Exception_isRuntime(x_24);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
lean_free_object(x_19);
lean_dec(x_24);
x_27 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_28 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__3(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_27, x_11, x_12, x_13, x_14, x_15, x_16, x_25);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_28;
}
else
{
uint8_t x_29;
x_29 = lean_ctor_get_uint8(x_15, sizeof(void*)*11);
if (x_29 == 0)
{
lean_dec(x_18);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_19;
}
else
{
lean_object* x_30; lean_object* x_31;
lean_free_object(x_19);
lean_dec(x_24);
x_30 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_31 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__3(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_30, x_11, x_12, x_13, x_14, x_15, x_16, x_25);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_31;
}
}
}
else
{
lean_object* x_32; lean_object* x_33; uint8_t x_34;
x_32 = lean_ctor_get(x_19, 0);
x_33 = lean_ctor_get(x_19, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_19, 1);
lean_inc(x_23);
lean_dec(x_19);
x_34 = l_Lean_Exception_isRuntime(x_32);
if (x_34 == 0)
{
lean_object* x_35; lean_object* x_36;
lean_dec(x_32);
x_35 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_36 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__3(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_35, x_11, x_12, x_13, x_14, x_15, x_16, x_33);
x_24 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_25 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__3(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_24, x_11, x_12, x_13, x_14, x_15, x_16, x_23);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_36;
}
else
{
uint8_t x_37;
x_37 = lean_ctor_get_uint8(x_15, sizeof(void*)*11);
if (x_37 == 0)
{
lean_object* x_38;
lean_dec(x_18);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_32);
lean_ctor_set(x_38, 1, x_33);
return x_38;
}
else
{
lean_object* x_39; lean_object* x_40;
lean_dec(x_32);
x_39 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_40 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__3(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_39, x_11, x_12, x_13, x_14, x_15, x_16, x_33);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_40;
}
}
}
return x_25;
}
}
}
@ -8649,12 +8493,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_tryRe
_start:
{
lean_object* x_7;
lean_inc(x_4);
x_7 = lean_apply_5(x_1, x_2, x_3, x_4, x_5, x_6);
if (lean_obj_tag(x_7) == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
@ -8687,83 +8529,28 @@ uint8_t x_15;
x_15 = !lean_is_exclusive(x_7);
if (x_15 == 0)
{
lean_object* x_16; uint8_t x_17;
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_7, 0);
x_17 = l_Lean_Exception_isRuntime(x_16);
if (x_17 == 0)
{
lean_object* x_18;
lean_dec(x_4);
x_18 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_18, 0, x_16);
x_17 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_18);
lean_ctor_set(x_7, 0, x_17);
return x_7;
}
else
{
uint8_t x_19;
x_19 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_19 == 0)
{
return x_7;
}
else
{
lean_object* x_20;
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_20);
return x_7;
}
}
}
else
{
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_7, 0);
x_22 = lean_ctor_get(x_7, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_7, 0);
x_19 = lean_ctor_get(x_7, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_7);
x_23 = l_Lean_Exception_isRuntime(x_21);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25;
lean_dec(x_4);
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_21);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_22);
return x_25;
}
else
{
uint8_t x_26;
x_26 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_26 == 0)
{
lean_object* x_27;
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_21);
lean_ctor_set(x_27, 1, x_22);
return x_27;
}
else
{
lean_object* x_28; lean_object* x_29;
x_28 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_28, 0, x_21);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_22);
return x_29;
}
}
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_18);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
}
@ -8887,111 +8674,16 @@ return x_20;
}
else
{
uint8_t x_21;
x_21 = !lean_is_exclusive(x_17);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_22 = lean_ctor_get(x_17, 0);
x_23 = lean_ctor_get(x_17, 1);
x_24 = l_Lean_Exception_isRuntime(x_22);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26;
lean_free_object(x_17);
lean_dec(x_22);
x_25 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_26 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_tryResolve___spec__2___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_25, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_26;
}
else
{
uint8_t x_27;
x_27 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_27 == 0)
{
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_17;
}
else
{
lean_object* x_28; lean_object* x_29;
lean_free_object(x_17);
lean_dec(x_22);
x_28 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_29 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_tryResolve___spec__2___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_28, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_29;
}
}
}
else
{
lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_30 = lean_ctor_get(x_17, 0);
x_31 = lean_ctor_get(x_17, 1);
lean_inc(x_31);
lean_inc(x_30);
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 1);
lean_inc(x_21);
lean_dec(x_17);
x_32 = l_Lean_Exception_isRuntime(x_30);
if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34;
lean_dec(x_30);
x_33 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_34 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_tryResolve___spec__2___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_33, x_11, x_12, x_13, x_14, x_31);
x_22 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_23 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_tryResolve___spec__2___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_22, x_11, x_12, x_13, x_14, x_21);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_34;
}
else
{
uint8_t x_35;
x_35 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_35 == 0)
{
lean_object* x_36;
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_30);
lean_ctor_set(x_36, 1, x_31);
return x_36;
}
else
{
lean_object* x_37; lean_object* x_38;
lean_dec(x_30);
x_37 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_38 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_tryResolve___spec__2___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_37, x_11, x_12, x_13, x_14, x_31);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_38;
}
}
}
return x_23;
}
}
}
@ -11190,115 +10882,16 @@ return x_22;
}
else
{
uint8_t x_23;
x_23 = !lean_is_exclusive(x_19);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_19, 0);
x_25 = lean_ctor_get(x_19, 1);
x_26 = l_Lean_Exception_isRuntime(x_24);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
lean_free_object(x_19);
lean_dec(x_24);
x_27 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_28 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_addAnswer___spec__3___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_27, x_11, x_12, x_13, x_14, x_15, x_16, x_25);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_28;
}
else
{
uint8_t x_29;
x_29 = lean_ctor_get_uint8(x_15, sizeof(void*)*11);
if (x_29 == 0)
{
lean_dec(x_18);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_19;
}
else
{
lean_object* x_30; lean_object* x_31;
lean_free_object(x_19);
lean_dec(x_24);
x_30 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_31 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_addAnswer___spec__3___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_30, x_11, x_12, x_13, x_14, x_15, x_16, x_25);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_31;
}
}
}
else
{
lean_object* x_32; lean_object* x_33; uint8_t x_34;
x_32 = lean_ctor_get(x_19, 0);
x_33 = lean_ctor_get(x_19, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_19, 1);
lean_inc(x_23);
lean_dec(x_19);
x_34 = l_Lean_Exception_isRuntime(x_32);
if (x_34 == 0)
{
lean_object* x_35; lean_object* x_36;
lean_dec(x_32);
x_35 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_36 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_addAnswer___spec__3___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_35, x_11, x_12, x_13, x_14, x_15, x_16, x_33);
x_24 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_25 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_addAnswer___spec__3___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_24, x_11, x_12, x_13, x_14, x_15, x_16, x_23);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_36;
}
else
{
uint8_t x_37;
x_37 = lean_ctor_get_uint8(x_15, sizeof(void*)*11);
if (x_37 == 0)
{
lean_object* x_38;
lean_dec(x_18);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_32);
lean_ctor_set(x_38, 1, x_33);
return x_38;
}
else
{
lean_object* x_39; lean_object* x_40;
lean_dec(x_32);
x_39 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_40 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_addAnswer___spec__3___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_39, x_11, x_12, x_13, x_14, x_15, x_16, x_33);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_40;
}
}
}
return x_25;
}
}
}
@ -17705,115 +17298,16 @@ return x_22;
}
else
{
uint8_t x_23;
x_23 = !lean_is_exclusive(x_19);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_19, 0);
x_25 = lean_ctor_get(x_19, 1);
x_26 = l_Lean_Exception_isRuntime(x_24);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
lean_free_object(x_19);
lean_dec(x_24);
x_27 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_28 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_generate___spec__1___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_27, x_11, x_12, x_13, x_14, x_15, x_16, x_25);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_28;
}
else
{
uint8_t x_29;
x_29 = lean_ctor_get_uint8(x_15, sizeof(void*)*11);
if (x_29 == 0)
{
lean_dec(x_18);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_19;
}
else
{
lean_object* x_30; lean_object* x_31;
lean_free_object(x_19);
lean_dec(x_24);
x_30 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_31 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_generate___spec__1___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_30, x_11, x_12, x_13, x_14, x_15, x_16, x_25);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_31;
}
}
}
else
{
lean_object* x_32; lean_object* x_33; uint8_t x_34;
x_32 = lean_ctor_get(x_19, 0);
x_33 = lean_ctor_get(x_19, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_19, 1);
lean_inc(x_23);
lean_dec(x_19);
x_34 = l_Lean_Exception_isRuntime(x_32);
if (x_34 == 0)
{
lean_object* x_35; lean_object* x_36;
lean_dec(x_32);
x_35 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_36 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_generate___spec__1___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_35, x_11, x_12, x_13, x_14, x_15, x_16, x_33);
x_24 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_25 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_generate___spec__1___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_24, x_11, x_12, x_13, x_14, x_15, x_16, x_23);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_36;
}
else
{
uint8_t x_37;
x_37 = lean_ctor_get_uint8(x_15, sizeof(void*)*11);
if (x_37 == 0)
{
lean_object* x_38;
lean_dec(x_18);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_32);
lean_ctor_set(x_38, 1, x_33);
return x_38;
}
else
{
lean_object* x_39; lean_object* x_40;
lean_dec(x_32);
x_39 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_40 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_generate___spec__1___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_39, x_11, x_12, x_13, x_14, x_15, x_16, x_33);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_4);
return x_40;
}
}
}
return x_25;
}
}
}
@ -24065,111 +23559,16 @@ return x_20;
}
else
{
uint8_t x_21;
x_21 = !lean_is_exclusive(x_17);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_22 = lean_ctor_get(x_17, 0);
x_23 = lean_ctor_get(x_17, 1);
x_24 = l_Lean_Exception_isRuntime(x_22);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26;
lean_free_object(x_17);
lean_dec(x_22);
x_25 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_26 = l_Lean_withTraceNode___at_Lean_Meta_synthInstance_x3f___spec__13___lambda__2(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_25, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_26;
}
else
{
uint8_t x_27;
x_27 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_27 == 0)
{
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_17;
}
else
{
lean_object* x_28; lean_object* x_29;
lean_free_object(x_17);
lean_dec(x_22);
x_28 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_29 = l_Lean_withTraceNode___at_Lean_Meta_synthInstance_x3f___spec__13___lambda__2(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_28, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_29;
}
}
}
else
{
lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_30 = lean_ctor_get(x_17, 0);
x_31 = lean_ctor_get(x_17, 1);
lean_inc(x_31);
lean_inc(x_30);
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 1);
lean_inc(x_21);
lean_dec(x_17);
x_32 = l_Lean_Exception_isRuntime(x_30);
if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34;
lean_dec(x_30);
x_33 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_34 = l_Lean_withTraceNode___at_Lean_Meta_synthInstance_x3f___spec__13___lambda__2(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_33, x_11, x_12, x_13, x_14, x_31);
x_22 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_23 = l_Lean_withTraceNode___at_Lean_Meta_synthInstance_x3f___spec__13___lambda__2(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_22, x_11, x_12, x_13, x_14, x_21);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_34;
}
else
{
uint8_t x_35;
x_35 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_35 == 0)
{
lean_object* x_36;
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_30);
lean_ctor_set(x_36, 1, x_31);
return x_36;
}
else
{
lean_object* x_37; lean_object* x_38;
lean_dec(x_30);
x_37 = l_Lean_withTraceNode___at_Lean_Meta_SynthInstance_newSubgoal___spec__9___lambda__4___closed__2;
x_38 = l_Lean_withTraceNode___at_Lean_Meta_synthInstance_x3f___spec__13___lambda__2(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_37, x_11, x_12, x_13, x_14, x_31);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_38;
}
}
}
return x_23;
}
}
}

203
stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c generated
View file

@ -20065,12 +20065,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___s
_start:
{
lean_object* x_10;
lean_inc(x_7);
x_10 = lean_apply_8(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_10) == 0)
{
uint8_t x_11;
lean_dec(x_7);
x_11 = !lean_is_exclusive(x_10);
if (x_11 == 0)
{
@ -20103,83 +20101,28 @@ uint8_t x_18;
x_18 = !lean_is_exclusive(x_10);
if (x_18 == 0)
{
lean_object* x_19; uint8_t x_20;
lean_object* x_19; lean_object* x_20;
x_19 = lean_ctor_get(x_10, 0);
x_20 = l_Lean_Exception_isRuntime(x_19);
if (x_20 == 0)
{
lean_object* x_21;
lean_dec(x_7);
x_21 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_21, 0, x_19);
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set_tag(x_10, 0);
lean_ctor_set(x_10, 0, x_21);
lean_ctor_set(x_10, 0, x_20);
return x_10;
}
else
{
uint8_t x_22;
x_22 = lean_ctor_get_uint8(x_7, sizeof(void*)*11);
lean_dec(x_7);
if (x_22 == 0)
{
return x_10;
}
else
{
lean_object* x_23;
x_23 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_23, 0, x_19);
lean_ctor_set_tag(x_10, 0);
lean_ctor_set(x_10, 0, x_23);
return x_10;
}
}
}
else
{
lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_24 = lean_ctor_get(x_10, 0);
x_25 = lean_ctor_get(x_10, 1);
lean_inc(x_25);
lean_inc(x_24);
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_21 = lean_ctor_get(x_10, 0);
x_22 = lean_ctor_get(x_10, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_dec(x_10);
x_26 = l_Lean_Exception_isRuntime(x_24);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
lean_dec(x_7);
x_27 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_27, 0, x_24);
x_28 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_25);
return x_28;
}
else
{
uint8_t x_29;
x_29 = lean_ctor_get_uint8(x_7, sizeof(void*)*11);
lean_dec(x_7);
if (x_29 == 0)
{
lean_object* x_30;
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_24);
lean_ctor_set(x_30, 1, x_25);
return x_30;
}
else
{
lean_object* x_31; lean_object* x_32;
x_31 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_31, 0, x_24);
x_32 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_25);
return x_32;
}
}
x_23 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_23, 0, x_21);
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_22);
return x_24;
}
}
}
@ -20371,121 +20314,17 @@ return x_23;
}
else
{
uint8_t x_24;
x_24 = !lean_is_exclusive(x_20);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26; uint8_t x_27;
x_25 = lean_ctor_get(x_20, 0);
x_26 = lean_ctor_get(x_20, 1);
x_27 = l_Lean_Exception_isRuntime(x_25);
if (x_27 == 0)
{
lean_object* x_28; lean_object* x_29;
lean_free_object(x_20);
lean_dec(x_25);
x_28 = l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___spec__1___lambda__4___closed__2;
x_29 = l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___spec__1___lambda__3(x_1, x_2, x_19, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_28, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_26);
lean_dec(x_17);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_29;
}
else
{
uint8_t x_30;
x_30 = lean_ctor_get_uint8(x_16, sizeof(void*)*11);
if (x_30 == 0)
{
lean_dec(x_19);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_20;
}
else
{
lean_object* x_31; lean_object* x_32;
lean_free_object(x_20);
lean_dec(x_25);
x_31 = l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___spec__1___lambda__4___closed__2;
x_32 = l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___spec__1___lambda__3(x_1, x_2, x_19, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_31, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_26);
lean_dec(x_17);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_32;
}
}
}
else
{
lean_object* x_33; lean_object* x_34; uint8_t x_35;
x_33 = lean_ctor_get(x_20, 0);
x_34 = lean_ctor_get(x_20, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_20, 1);
lean_inc(x_24);
lean_dec(x_20);
x_35 = l_Lean_Exception_isRuntime(x_33);
if (x_35 == 0)
{
lean_object* x_36; lean_object* x_37;
lean_dec(x_33);
x_36 = l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___spec__1___lambda__4___closed__2;
x_37 = l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___spec__1___lambda__3(x_1, x_2, x_19, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_36, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_34);
x_25 = l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___spec__1___lambda__4___closed__2;
x_26 = l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___spec__1___lambda__3(x_1, x_2, x_19, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_25, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_24);
lean_dec(x_17);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_37;
}
else
{
uint8_t x_38;
x_38 = lean_ctor_get_uint8(x_16, sizeof(void*)*11);
if (x_38 == 0)
{
lean_object* x_39;
lean_dec(x_19);
lean_dec(x_17);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_33);
lean_ctor_set(x_39, 1, x_34);
return x_39;
}
else
{
lean_object* x_40; lean_object* x_41;
lean_dec(x_33);
x_40 = l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___spec__1___lambda__4___closed__2;
x_41 = l_Lean_withTraceNode___at_Lean_Meta_Simp_simpGround___spec__1___lambda__3(x_1, x_2, x_19, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_40, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_34);
lean_dec(x_17);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_41;
}
}
}
return x_26;
}
}
}

194
stage0/stdlib/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.c generated
View file

@ -30927,12 +30927,10 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborato
_start:
{
lean_object* x_7;
lean_inc(x_4);
x_7 = lean_apply_5(x_1, x_2, x_3, x_4, x_5, x_6);
if (lean_obj_tag(x_7) == 0)
{
uint8_t x_8;
lean_dec(x_4);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
@ -30965,83 +30963,28 @@ uint8_t x_15;
x_15 = !lean_is_exclusive(x_7);
if (x_15 == 0)
{
lean_object* x_16; uint8_t x_17;
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_7, 0);
x_17 = l_Lean_Exception_isRuntime(x_16);
if (x_17 == 0)
{
lean_object* x_18;
lean_dec(x_4);
x_18 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_18, 0, x_16);
x_17 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_18);
lean_ctor_set(x_7, 0, x_17);
return x_7;
}
else
{
uint8_t x_19;
x_19 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_19 == 0)
{
return x_7;
}
else
{
lean_object* x_20;
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_16);
lean_ctor_set_tag(x_7, 0);
lean_ctor_set(x_7, 0, x_20);
return x_7;
}
}
}
else
{
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_7, 0);
x_22 = lean_ctor_get(x_7, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_7, 0);
x_19 = lean_ctor_get(x_7, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_7);
x_23 = l_Lean_Exception_isRuntime(x_21);
if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25;
lean_dec(x_4);
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_21);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_22);
return x_25;
}
else
{
uint8_t x_26;
x_26 = lean_ctor_get_uint8(x_4, sizeof(void*)*11);
lean_dec(x_4);
if (x_26 == 0)
{
lean_object* x_27;
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_21);
lean_ctor_set(x_27, 1, x_22);
return x_27;
}
else
{
lean_object* x_28; lean_object* x_29;
x_28 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_28, 0, x_21);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_22);
return x_29;
}
}
x_20 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_20, 0, x_18);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
}
@ -31224,111 +31167,16 @@ return x_20;
}
else
{
uint8_t x_21;
x_21 = !lean_is_exclusive(x_17);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_22 = lean_ctor_get(x_17, 0);
x_23 = lean_ctor_get(x_17, 1);
x_24 = l_Lean_Exception_isRuntime(x_22);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26;
lean_free_object(x_17);
lean_dec(x_22);
x_25 = l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborator_topDownAnalyze___spec__2___lambda__4___closed__2;
x_26 = l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborator_topDownAnalyze___spec__2___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_25, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_26;
}
else
{
uint8_t x_27;
x_27 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_27 == 0)
{
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_17;
}
else
{
lean_object* x_28; lean_object* x_29;
lean_free_object(x_17);
lean_dec(x_22);
x_28 = l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborator_topDownAnalyze___spec__2___lambda__4___closed__2;
x_29 = l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborator_topDownAnalyze___spec__2___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_28, x_11, x_12, x_13, x_14, x_23);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_29;
}
}
}
else
{
lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_30 = lean_ctor_get(x_17, 0);
x_31 = lean_ctor_get(x_17, 1);
lean_inc(x_31);
lean_inc(x_30);
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 1);
lean_inc(x_21);
lean_dec(x_17);
x_32 = l_Lean_Exception_isRuntime(x_30);
if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34;
lean_dec(x_30);
x_33 = l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborator_topDownAnalyze___spec__2___lambda__4___closed__2;
x_34 = l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborator_topDownAnalyze___spec__2___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_33, x_11, x_12, x_13, x_14, x_31);
x_22 = l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborator_topDownAnalyze___spec__2___lambda__4___closed__2;
x_23 = l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborator_topDownAnalyze___spec__2___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_22, x_11, x_12, x_13, x_14, x_21);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_34;
}
else
{
uint8_t x_35;
x_35 = lean_ctor_get_uint8(x_13, sizeof(void*)*11);
if (x_35 == 0)
{
lean_object* x_36;
lean_dec(x_16);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_30);
lean_ctor_set(x_36, 1, x_31);
return x_36;
}
else
{
lean_object* x_37; lean_object* x_38;
lean_dec(x_30);
x_37 = l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborator_topDownAnalyze___spec__2___lambda__4___closed__2;
x_38 = l_Lean_withTraceNode___at_Lean_PrettyPrinter_Delaborator_topDownAnalyze___spec__2___lambda__3(x_1, x_2, x_16, x_3, x_4, x_5, x_6, x_7, lean_box(0), x_37, x_11, x_12, x_13, x_14, x_31);
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_4);
return x_38;
}
}
}
return x_23;
}
}
}

2458
stage0/stdlib/Lean/Util/Trace.c generated
View file

File diff suppressed because it is too large Load diff

1838
stage0/stdlib/Lean/Widget/UserWidget.c generated
View file

File diff suppressed because it is too large Load diff