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:
Scott Morrison 2024-02-01 11:29:05 +11:00 • committed by Scott Morrison
parent c4e6e48690
commit 8037a8733d
19 changed files with 17104 additions and 11778 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2775
stage0/stdlib/Init/Simproc.c generated
View file

File diff suppressed because it is too large Load diff

56
stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c generated
View file

@ -24,7 +24,6 @@ static lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition
static lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Eqns___hyg_1442____closed__13;
static lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Eqns___hyg_1215____closed__4;
LEAN_EXPORT lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Eqns___hyg_1215_(lean_object*);
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__16;
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__5;
lean_object* l_Lean_Meta_lambdaTelescope___at___private_Lean_Meta_Eqns_0__Lean_Meta_mkSimpleEqThm___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint32_t l_UInt32_ofNatTruncate(lean_object*);
@ -39,7 +38,6 @@ uint8_t lean_usize_dec_eq(size_t, size_t);
LEAN_EXPORT lean_object* lean_get_structural_rec_arg_pos(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Structural_instInhabitedEqnInfo;
LEAN_EXPORT lean_object* l_Lean_Elab_Structural_registerEqnsInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PersistentHashMap_empty___at_Lean_KeyedDeclsAttribute_ExtensionState_declNames___default___spec__1;
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__6;
lean_object* l_Lean_Expr_bvar___override(lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
@ -76,7 +74,6 @@ static lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__4;
static lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Eqns___hyg_1442____closed__4;
static lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Eqns___hyg_1442____closed__18;
lean_object* l_Lean_Meta_DiscrTree_empty(lean_object*);
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___closed__4;
lean_object* lean_st_ref_get(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__8;
@ -167,7 +164,6 @@ static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_
static lean_object* l_Lean_Elab_Structural_instInhabitedEqnInfo___closed__2;
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__13;
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__7;
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__17;
static lean_object* _init_l_Lean_Elab_Structural_instInhabitedEqnInfo___closed__1() {
_start:
{
@ -486,29 +482,24 @@ static lean_object* _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0_
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_DiscrTree_empty(lean_box(0));
x_1 = lean_mk_string_from_bytes("failed to generate equational theorem for '", 43);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__10;
x_2 = l_Lean_PersistentHashMap_empty___at_Lean_KeyedDeclsAttribute_ExtensionState_declNames___default___spec__1;
x_3 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set(x_3, 2, x_2);
lean_ctor_set(x_3, 3, x_2);
return x_3;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__12() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("failed to generate equational theorem for '", 43);
x_1 = lean_mk_string_from_bytes("'\n", 2);
return x_1;
}
}
@ -525,7 +516,7 @@ static lean_object* _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0_
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("'\n", 2);
x_1 = lean_mk_string_from_bytes("", 0);
return x_1;
}
}
@ -538,23 +529,6 @@ x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__16() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("", 0);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__16;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
@ -651,7 +625,7 @@ lean_inc(x_25);
lean_dec(x_23);
x_26 = lean_box(0);
x_27 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__9;
x_28 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__11;
x_28 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__3;
x_29 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__4;
lean_inc(x_7);
lean_inc(x_6);
@ -760,11 +734,11 @@ x_49 = lean_ctor_get(x_47, 1);
lean_inc(x_49);
lean_dec(x_47);
x_50 = l_Lean_MessageData_ofName(x_2);
x_51 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__13;
x_51 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__11;
x_52 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_52, 0, x_51);
lean_ctor_set(x_52, 1, x_50);
x_53 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__15;
x_53 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__13;
x_54 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
@ -773,7 +747,7 @@ lean_ctor_set(x_55, 0, x_1);
x_56 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);
x_57 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__17;
x_57 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__15;
x_58 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_58, 0, x_56);
lean_ctor_set(x_58, 1, x_57);
@ -1417,7 +1391,7 @@ x_17 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structur
x_18 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_16);
x_19 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__17;
x_19 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__15;
x_20 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_20, 0, x_18);
lean_ctor_set(x_20, 1, x_19);
@ -1727,7 +1701,7 @@ x_17 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structur
x_18 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_16);
x_19 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__17;
x_19 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__15;
x_20 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_20, 0, x_18);
lean_ctor_set(x_20, 1, x_19);
@ -2081,7 +2055,7 @@ else
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51;
lean_inc(x_24);
x_44 = l_Lean_MessageData_ofExpr(x_24);
x_45 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__17;
x_45 = l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__15;
x_46 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_44);
@ -3598,10 +3572,6 @@ l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkPr
lean_mark_persistent(l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__14);
l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__15 = _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__15();
lean_mark_persistent(l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__15);
l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__16 = _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__16();
lean_mark_persistent(l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__16);
l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__17 = _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__17();
lean_mark_persistent(l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__17);
l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___closed__1 = _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___closed__1();
lean_mark_persistent(l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___closed__1);
l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___closed__2 = _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___closed__2();

38
stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c generated
View file

@ -29,7 +29,6 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_rwFixEq___lambda__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_WF_instInhabitedEqnInfo;
static lean_object* l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__10;
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_WF_registerEqnsInfo___closed__13;
static lean_object* l_Lean_Elab_WF_initFn____x40_Lean_Elab_PreDefinition_WF_Eqns___hyg_2330____closed__5;
@ -64,7 +63,6 @@ static lean_object* l_Lean_Elab_WF_registerEqnsInfo___closed__11;
lean_object* lean_mk_array(lean_object*, lean_object*);
uint8_t lean_usize_dec_eq(size_t, size_t);
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_deltaLHSUntilFix___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PersistentHashMap_empty___at_Lean_KeyedDeclsAttribute_ExtensionState_declNames___default___spec__1;
lean_object* l_Lean_MVarId_getType_x27(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_getFixedPrefix___lambda__2___closed__6;
static lean_object* l_Lean_Elab_WF_registerEqnsInfo___closed__10;
@ -129,10 +127,8 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Ela
lean_object* l_Lean_MVarId_withContext___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Match_MatcherInfo_numAlts(lean_object*);
static lean_object* l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_getFixedPrefix___lambda__3___closed__6;
lean_object* l_Lean_Meta_DiscrTree_empty(lean_object*);
static lean_object* l_Lean_Elab_WF_registerEqnsInfo___closed__7;
LEAN_EXPORT lean_object* l_Lean_Elab_WF_simpMatchWF_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__11;
LEAN_EXPORT lean_object* l_panic___at___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_getFixedPrefix___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkEqTrans(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2648,37 +2644,15 @@ static lean_object* _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_El
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_DiscrTree_empty(lean_box(0));
x_1 = lean_mk_string_from_bytes("'\n", 2);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__8;
x_2 = l_Lean_PersistentHashMap_empty___at_Lean_KeyedDeclsAttribute_ExtensionState_declNames___default___spec__1;
x_3 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set(x_3, 2, x_2);
lean_ctor_set(x_3, 3, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__10() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("'\n", 2);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__10;
x_1 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__8;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
@ -2779,7 +2753,7 @@ lean_inc(x_25);
lean_dec(x_23);
x_26 = lean_box(0);
x_27 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__7;
x_28 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__9;
x_28 = l_Lean_Elab_WF_instInhabitedEqnInfo___closed__3;
x_29 = l_Lean_Elab_WF_simpMatchWF_x3f___lambda__3___closed__1;
lean_inc(x_7);
lean_inc(x_6);
@ -2874,7 +2848,7 @@ x_48 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_getFixedPrefi
x_49 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_49, 0, x_48);
lean_ctor_set(x_49, 1, x_47);
x_50 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__11;
x_50 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__9;
x_51 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
@ -6128,10 +6102,6 @@ l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda_
lean_mark_persistent(l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__8);
l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__9 = _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__9();
lean_mark_persistent(l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__9);
l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__10 = _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__10();
lean_mark_persistent(l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__10);
l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__11 = _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__11();
lean_mark_persistent(l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__11);
l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___closed__1 = _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___closed__1();
lean_mark_persistent(l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___closed__1);
l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___closed__2 = _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___closed__2();

2229
stage0/stdlib/Lean/Elab/Tactic/Simp.c generated
View file

File diff suppressed because it is too large Load diff

1314
stage0/stdlib/Lean/Elab/Tactic/Simproc.c generated
View file

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean/Linter/MissingDocs.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Linter.MissingDocs
// Imports: Init Lean.Meta.Tactic.Simp.SimpTheorems Lean.Elab.Command Lean.Elab.SetOption Lean.Linter.Util
// Imports: Init Lean.Meta.Tactic.Simp.RegisterCommand Lean.Elab.Command Lean.Elab.SetOption Lean.Linter.Util
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -8525,7 +8525,7 @@ return x_4;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Simp_SimpTheorems(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Simp_RegisterCommand(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_Command(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_SetOption(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Linter_Util(uint8_t builtin, lean_object*);
@ -8537,7 +8537,7 @@ _G_initialized = true;
res = initialize_Init(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_Simp_SimpTheorems(builtin, lean_io_mk_world());
res = initialize_Lean_Meta_Tactic_Simp_RegisterCommand(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Command(builtin, lean_io_mk_world());

64
stage0/stdlib/Lean/Meta/Tactic/Acyclic.c generated
View file

@ -29,7 +29,6 @@ static lean_object* l_Lean_MVarId_acyclic_go___closed__22;
uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_MVarId_acyclic_go___closed__17;
lean_object* lean_array_push(lean_object*, lean_object*);
static lean_object* l_Lean_MVarId_acyclic_go___closed__32;
static lean_object* l_Lean_MVarId_initFn____x40_Lean_Meta_Tactic_Acyclic___hyg_879____closed__8;
static lean_object* l_Lean_MVarId_initFn____x40_Lean_Meta_Tactic_Acyclic___hyg_879____closed__16;
LEAN_EXPORT lean_object* l_Lean_MVarId_acyclic_go___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -55,7 +54,6 @@ static lean_object* l_Lean_MVarId_initFn____x40_Lean_Meta_Tactic_Acyclic___hyg_8
static lean_object* l_Lean_MVarId_acyclic_go___closed__26;
lean_object* l_Lean_MVarId_withContext___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_simpTarget(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_DiscrTree_empty(lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkAppM(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_MVarId_initFn____x40_Lean_Meta_Tactic_Acyclic___hyg_879____closed__12;
@ -111,7 +109,6 @@ lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_obje
static lean_object* l_Lean_MVarId_acyclic_go___closed__7;
static lean_object* l_Lean_MVarId_acyclic_go___closed__6;
uint8_t l_Lean_Exception_isRuntime(lean_object*);
extern lean_object* l_Lean_PersistentHashMap_empty___at_Lean_Meta_Instances_erased___default___spec__1;
uint8_t l_Lean_Expr_isFVar(lean_object*);
lean_object* l_Lean_Expr_mvarId_x21(lean_object*);
LEAN_EXPORT lean_object* l_Lean_MVarId_acyclic___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -476,34 +473,21 @@ return x_4;
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__22() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_DiscrTree_empty(lean_box(0));
return x_1;
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__23() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_MVarId_acyclic_go___closed__22;
x_2 = l_Lean_PersistentHashMap_empty___at_Lean_Meta_Instances_erased___default___spec__1;
x_3 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set(x_3, 2, x_2);
lean_ctor_set(x_3, 3, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__24() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("Nat", 3);
return x_1;
}
}
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__25() {
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__24() {
_start:
{
lean_object* x_1;
@ -511,17 +495,17 @@ x_1 = lean_mk_string_from_bytes("lt_of_lt_of_eq", 14);
return x_1;
}
}
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__26() {
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__25() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_MVarId_acyclic_go___closed__24;
x_2 = l_Lean_MVarId_acyclic_go___closed__25;
x_1 = l_Lean_MVarId_acyclic_go___closed__23;
x_2 = l_Lean_MVarId_acyclic_go___closed__24;
x_3 = l_Lean_Name_mkStr2(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__27() {
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__26() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -530,7 +514,7 @@ x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__28() {
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__27() {
_start:
{
lean_object* x_1;
@ -538,17 +522,17 @@ x_1 = lean_mk_string_from_bytes("lt_irrefl", 9);
return x_1;
}
}
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__29() {
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__28() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_MVarId_acyclic_go___closed__24;
x_2 = l_Lean_MVarId_acyclic_go___closed__28;
x_1 = l_Lean_MVarId_acyclic_go___closed__23;
x_2 = l_Lean_MVarId_acyclic_go___closed__27;
x_3 = l_Lean_Name_mkStr2(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__30() {
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__29() {
_start:
{
lean_object* x_1;
@ -556,7 +540,7 @@ x_1 = lean_alloc_closure((void*)(l_Lean_MVarId_acyclic_go___lambda__2___boxed),
return x_1;
}
}
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__31() {
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__30() {
_start:
{
lean_object* x_1;
@ -564,11 +548,11 @@ x_1 = lean_mk_string_from_bytes("succeeded", 9);
return x_1;
}
}
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__32() {
static lean_object* _init_l_Lean_MVarId_acyclic_go___closed__31() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_MVarId_acyclic_go___closed__31;
x_1 = l_Lean_MVarId_acyclic_go___closed__30;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
@ -653,7 +637,7 @@ lean_ctor_set(x_111, 3, x_105);
lean_ctor_set_uint8(x_111, sizeof(void*)*4 + 8, x_108);
lean_ctor_set_uint32(x_111, sizeof(void*)*4, x_109);
lean_ctor_set_uint32(x_111, sizeof(void*)*4 + 4, x_106);
x_112 = l_Lean_MVarId_acyclic_go___closed__23;
x_112 = l_Lean_MVarId_acyclic_go___closed__22;
x_113 = 1;
x_114 = l_Lean_MVarId_acyclic_go___closed__17;
lean_inc(x_8);
@ -702,10 +686,10 @@ lean_inc(x_124);
x_125 = lean_ctor_get(x_123, 1);
lean_inc(x_125);
lean_dec(x_123);
x_126 = l_Lean_MVarId_acyclic_go___closed__27;
x_126 = l_Lean_MVarId_acyclic_go___closed__26;
x_127 = lean_array_push(x_126, x_97);
x_128 = lean_array_push(x_127, x_124);
x_129 = l_Lean_MVarId_acyclic_go___closed__26;
x_129 = l_Lean_MVarId_acyclic_go___closed__25;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
@ -720,7 +704,7 @@ x_132 = lean_ctor_get(x_130, 1);
lean_inc(x_132);
lean_dec(x_130);
x_133 = lean_array_push(x_82, x_86);
x_134 = l_Lean_MVarId_acyclic_go___closed__29;
x_134 = l_Lean_MVarId_acyclic_go___closed__28;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
@ -769,7 +753,7 @@ lean_inc(x_149);
x_150 = lean_ctor_get(x_148, 1);
lean_inc(x_150);
lean_dec(x_148);
x_151 = l_Lean_MVarId_acyclic_go___closed__30;
x_151 = l_Lean_MVarId_acyclic_go___closed__29;
x_152 = lean_unbox(x_149);
lean_dec(x_149);
if (x_152 == 0)
@ -823,7 +807,7 @@ goto block_81;
else
{
lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165;
x_161 = l_Lean_MVarId_acyclic_go___closed__32;
x_161 = l_Lean_MVarId_acyclic_go___closed__31;
x_162 = l_Lean_addTrace___at_Lean_Meta_processPostponed_loop___spec__2(x_147, x_161, x_5, x_6, x_7, x_8, x_150);
x_163 = lean_ctor_get(x_162, 0);
lean_inc(x_163);
@ -2031,8 +2015,6 @@ l_Lean_MVarId_acyclic_go___closed__30 = _init_l_Lean_MVarId_acyclic_go___closed_
lean_mark_persistent(l_Lean_MVarId_acyclic_go___closed__30);
l_Lean_MVarId_acyclic_go___closed__31 = _init_l_Lean_MVarId_acyclic_go___closed__31();
lean_mark_persistent(l_Lean_MVarId_acyclic_go___closed__31);
l_Lean_MVarId_acyclic_go___closed__32 = _init_l_Lean_MVarId_acyclic_go___closed__32();
lean_mark_persistent(l_Lean_MVarId_acyclic_go___closed__32);
l_Lean_MVarId_acyclic___lambda__1___closed__1 = _init_l_Lean_MVarId_acyclic___lambda__1___closed__1();
lean_mark_persistent(l_Lean_MVarId_acyclic___lambda__1___closed__1);
l_Lean_MVarId_acyclic___lambda__1___closed__2 = _init_l_Lean_MVarId_acyclic___lambda__1___closed__2();

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

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Meta.Tactic.Simp
// Imports: Init Lean.Meta.Tactic.Simp.SimpTheorems Lean.Meta.Tactic.Simp.SimpCongrTheorems Lean.Meta.Tactic.Simp.Types Lean.Meta.Tactic.Simp.Main Lean.Meta.Tactic.Simp.Rewrite Lean.Meta.Tactic.Simp.SimpAll Lean.Meta.Tactic.Simp.Simproc Lean.Meta.Tactic.Simp.BuiltinSimprocs
// Imports: Init Lean.Meta.Tactic.Simp.SimpTheorems Lean.Meta.Tactic.Simp.SimpCongrTheorems Lean.Meta.Tactic.Simp.Types Lean.Meta.Tactic.Simp.Main Lean.Meta.Tactic.Simp.Rewrite Lean.Meta.Tactic.Simp.SimpAll Lean.Meta.Tactic.Simp.Simproc Lean.Meta.Tactic.Simp.BuiltinSimprocs Lean.Meta.Tactic.Simp.RegisterCommand
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -620,6 +620,7 @@ lean_object* initialize_Lean_Meta_Tactic_Simp_Rewrite(uint8_t builtin, lean_obje
lean_object* initialize_Lean_Meta_Tactic_Simp_SimpAll(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Simp_Simproc(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Simp_RegisterCommand(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Meta_Tactic_Simp(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -652,6 +653,9 @@ lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_Simp_RegisterCommand(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_initFn____x40_Lean_Meta_Tactic_Simp___hyg_4____closed__1 = _init_l_Lean_initFn____x40_Lean_Meta_Tactic_Simp___hyg_4____closed__1();
lean_mark_persistent(l_Lean_initFn____x40_Lean_Meta_Tactic_Simp___hyg_4____closed__1);
l_Lean_initFn____x40_Lean_Meta_Tactic_Simp___hyg_4____closed__2 = _init_l_Lean_initFn____x40_Lean_Meta_Tactic_Simp___hyg_4____closed__2();

42
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.c generated
View file

@ -40,6 +40,7 @@ static lean_object* l_reduceDite___lambda__2___closed__1;
static lean_object* l_reduceDite___closed__2;
static lean_object* l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_254____closed__4;
static lean_object* l_reduceIte___lambda__1___closed__1;
extern lean_object* l_Lean_Meta_Simp_builtinSimprocsRef;
lean_object* l_Lean_Expr_getRevArg_x21(lean_object*, lean_object*);
static lean_object* l___regBuiltin_reduceDite_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_532____closed__7;
static lean_object* l_reduceDite___lambda__2___closed__3;
@ -47,6 +48,7 @@ static lean_object* l___regBuiltin_reduceDite_declare____x40_Lean_Meta_Tactic_Si
LEAN_EXPORT lean_object* l___regBuiltin_reduceDite_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_534_(lean_object*);
static lean_object* l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_254____closed__1;
static lean_object* l_reduceIte___lambda__3___closed__1;
static lean_object* l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_256____closed__1;
static lean_object* l_reduceIte___lambda__3___closed__2;
LEAN_EXPORT lean_object* l___regBuiltin_reduceDite_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_532_(lean_object*);
static lean_object* l___regBuiltin_reduceDite_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_532____closed__3;
@ -73,6 +75,7 @@ static lean_object* l_reduceIte___closed__1;
lean_object* l_Lean_Meta_Simp_registerBuiltinSimproc(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_reduceIte___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_reduceDite___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_reduceIte(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_reduceIte___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_reduceIte___lambda__3___closed__4;
@ -84,7 +87,6 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn(lean_object*);
static lean_object* l_reduceDite___lambda__2___closed__4;
LEAN_EXPORT lean_object* l_reduceIte___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_addSimprocBuiltinAttr(lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_254_(lean_object*);
static lean_object* l_reduceDite___lambda__1___closed__3;
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
@ -701,15 +703,24 @@ x_5 = l_Lean_Meta_Simp_registerBuiltinSimproc(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_256____closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_Simp_builtinSimprocsRef;
return x_1;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_256_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_254____closed__2;
x_3 = 0;
x_4 = l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_254____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_256____closed__1;
x_3 = l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_254____closed__2;
x_4 = 0;
x_5 = l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_254____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
static lean_object* _init_l_reduceDite___lambda__1___closed__1() {
@ -1313,12 +1324,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_reduceDite_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_534_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_reduceDite_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_532____closed__2;
x_3 = 0;
x_4 = l___regBuiltin_reduceDite_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_532____closed__10;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_256____closed__1;
x_3 = l___regBuiltin_reduceDite_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_532____closed__2;
x_4 = 0;
x_5 = l___regBuiltin_reduceDite_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_532____closed__10;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
@ -1385,7 +1397,9 @@ lean_mark_persistent(l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Si
if (builtin) {res = l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_254_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}if (builtin) {res = l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_256_(lean_io_mk_world());
}l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_256____closed__1 = _init_l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_256____closed__1();
lean_mark_persistent(l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_256____closed__1);
if (builtin) {res = l___regBuiltin_reduceIte_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core___hyg_256_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}l_reduceDite___lambda__1___closed__1 = _init_l_reduceDite___lambda__1___closed__1();

146
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.c generated
View file

@ -103,6 +103,7 @@ static lean_object* l___regBuiltin_Fin_reduceLE_declare____x40_Lean_Meta_Tactic_
static lean_object* l_Fin_reduceLT___closed__2;
static lean_object* l_Fin_Value_toExpr___closed__1;
static lean_object* l_Fin_reduceBinPred___lambda__1___closed__13;
extern lean_object* l_Lean_Meta_Simp_builtinSimprocsRef;
LEAN_EXPORT lean_object* l_Fin_reduceBinPred___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Fin_fromExpr_x3f___closed__2;
@ -208,6 +209,7 @@ static lean_object* l___regBuiltin_Fin_reduceLE_declare____x40_Lean_Meta_Tactic_
lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Fin_reduceAdd___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkEqRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
static lean_object* l_Fin_reduceBinPred___lambda__1___closed__6;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_973_(lean_object*);
static lean_object* l_Fin_reduceLE___closed__3;
@ -225,7 +227,6 @@ static lean_object* l___regBuiltin_Fin_reduceSub_declare____x40_Lean_Meta_Tactic
static lean_object* l_Fin_reduceSub___closed__2;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_893_(lean_object*);
static lean_object* l_Fin_reduceLE___closed__1;
lean_object* l_Lean_Meta_Simp_addSimprocBuiltinAttr(lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Fin_reduceGT___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Fin_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_812____closed__10;
static lean_object* l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_695____closed__12;
@ -250,6 +251,7 @@ lean_object* l_Nat_fromExpr_x3f(lean_object*, lean_object*, lean_object*, lean_o
static lean_object* l_Fin_reduceBinPred___lambda__1___closed__12;
LEAN_EXPORT lean_object* l_Fin_reduceSub___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Fin_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_734____closed__11;
static lean_object* l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
static lean_object* l___regBuiltin_Fin_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_891____closed__1;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Fin_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_773____closed__12;
@ -2988,15 +2990,24 @@ x_5 = l_Lean_Meta_Simp_registerBuiltinSimproc(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_Simp_builtinSimprocsRef;
return x_1;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_695____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_695____closed__16;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
x_3 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_695____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_695____closed__16;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Fin_reduceMul___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
@ -3570,12 +3581,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_736_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Fin_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_734____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Fin_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_734____closed__14;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
x_3 = l___regBuiltin_Fin_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_734____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Fin_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_734____closed__14;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Fin_reduceSub___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
@ -4149,12 +4161,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_775_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Fin_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_773____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Fin_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_773____closed__14;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
x_3 = l___regBuiltin_Fin_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_773____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Fin_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_773____closed__14;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Fin_reduceDiv___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
@ -4728,12 +4741,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_814_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Fin_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_812____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Fin_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_812____closed__14;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
x_3 = l___regBuiltin_Fin_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_812____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Fin_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_812____closed__14;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Fin_reduceMod___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
@ -5307,12 +5321,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_853_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Fin_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_851____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Fin_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_851____closed__14;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
x_3 = l___regBuiltin_Fin_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_851____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Fin_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_851____closed__14;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Fin_reduceLT___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -6129,12 +6144,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_893_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Fin_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_891____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Fin_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_891____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
x_3 = l___regBuiltin_Fin_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_891____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Fin_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_891____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Fin_reduceLE___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -6942,12 +6958,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_933_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Fin_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_931____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Fin_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_931____closed__10;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
x_3 = l___regBuiltin_Fin_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_931____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Fin_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_931____closed__10;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Fin_reduceGT___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -7683,12 +7700,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_973_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Fin_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_971____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Fin_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_971____closed__3;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
x_3 = l___regBuiltin_Fin_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_971____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Fin_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_971____closed__3;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Fin_reduceGE___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -8424,12 +8442,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_1013_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Fin_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_1011____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Fin_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_1011____closed__3;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
x_3 = l___regBuiltin_Fin_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_1011____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Fin_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_1011____closed__3;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Fin_isValue___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -8617,12 +8636,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Fin_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_1086_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Fin_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_1084____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Fin_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_1084____closed__10;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1;
x_3 = l___regBuiltin_Fin_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_1084____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Fin_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_1084____closed__10;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
@ -8743,7 +8763,9 @@ lean_mark_persistent(l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tacti
if (builtin) {res = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_695_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}if (builtin) {res = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697_(lean_io_mk_world());
}l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1 = _init_l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1();
lean_mark_persistent(l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697____closed__1);
if (builtin) {res = l___regBuiltin_Fin_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin___hyg_697_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}l_Fin_reduceMul___closed__1 = _init_l_Fin_reduceMul___closed__1();

185
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.c generated
View file

@ -118,6 +118,7 @@ LEAN_EXPORT lean_object* l_Int_fromExpr_x3f___lambda__2(lean_object*, uint8_t, l
LEAN_EXPORT lean_object* l_Int_reduceNeg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Int_isPosValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1095____closed__6;
LEAN_EXPORT lean_object* l_Int_reduceLE(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_Simp_builtinSimprocsRef;
static lean_object* l___regBuiltin_Int_reduceAbs_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1552____closed__6;
static lean_object* l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1023____closed__1;
static lean_object* l___regBuiltin_Int_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1591____closed__8;
@ -245,6 +246,7 @@ static lean_object* l_Int_toExpr___closed__6;
static lean_object* l_Int_reduceAbs___closed__1;
static lean_object* l_Int_reduceBinPred___lambda__1___closed__2;
lean_object* l_Lean_Meta_mkEqRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_reduceMul___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Int_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1630____closed__1;
static lean_object* l_Int_reduceLT___closed__1;
@ -270,6 +272,7 @@ static lean_object* l___regBuiltin_Int_isPosValue_declare____x40_Lean_Meta_Tacti
lean_object* lean_int_mod(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Int_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1171____closed__2;
static lean_object* l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1023____closed__10;
static lean_object* l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
static lean_object* l_Int_reduceGT___closed__3;
LEAN_EXPORT lean_object* l_Int_reduceSub(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Int_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1133____closed__12;
@ -281,7 +284,6 @@ LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceLT_declare____x40_Lean_Meta_Ta
static lean_object* l___regBuiltin_Int_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1630____closed__7;
static lean_object* l___regBuiltin_Int_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1171____closed__1;
static lean_object* l___regBuiltin_Int_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1630____closed__9;
lean_object* l_Lean_Meta_Simp_addSimprocBuiltinAttr(lean_object*, uint8_t, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Int_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1209____closed__8;
static lean_object* l___regBuiltin_Int_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1591____closed__5;
static lean_object* l___regBuiltin_Int_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1247____closed__2;
@ -2674,15 +2676,24 @@ x_5 = l_Lean_Meta_Simp_registerBuiltinSimproc(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_Simp_builtinSimprocsRef;
return x_1;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1023____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1023____closed__10;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1023____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1023____closed__10;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_isPosValue(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
@ -2818,12 +2829,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_isPosValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1097_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_isPosValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1095____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_isPosValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1095____closed__8;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_isPosValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1095____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_isPosValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1095____closed__8;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reduceAdd___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -3243,12 +3255,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1135_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1133____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1133____closed__12;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1133____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1133____closed__12;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reduceMul___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -3659,12 +3672,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1173_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1171____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1171____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1171____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1171____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reduceSub___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -4075,12 +4089,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1211_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1209____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1209____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1209____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1209____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reduceDiv___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -4491,12 +4506,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1249_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1247____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1247____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1247____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1247____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reduceMod___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -4907,12 +4923,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1287_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1285____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1285____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1285____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1285____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reducePow___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -5357,12 +5374,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reducePow_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1445_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reducePow_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1443____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reducePow_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1443____closed__14;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reducePow_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1443____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reducePow_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1443____closed__14;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reduceAbs___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -5629,12 +5647,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceAbs_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1554_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceAbs_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1552____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceAbs_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1552____closed__7;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceAbs_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1552____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceAbs_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1552____closed__7;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reduceLT___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -6430,12 +6449,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1593_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1591____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1591____closed__10;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1591____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1591____closed__10;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reduceLE___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -7222,12 +7242,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1632_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1630____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1630____closed__9;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1630____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1630____closed__9;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reduceGT___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -7952,12 +7973,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1671_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1669____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1669____closed__3;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1669____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1669____closed__3;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Int_reduceGE___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -8682,12 +8704,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Int_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1710_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Int_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1708____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Int_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1708____closed__3;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1;
x_3 = l___regBuiltin_Int_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1708____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Int_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1708____closed__3;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
@ -8820,7 +8843,9 @@ lean_mark_persistent(l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tacti
if (builtin) {res = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1023_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}if (builtin) {res = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025_(lean_io_mk_world());
}l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1 = _init_l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1();
lean_mark_persistent(l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025____closed__1);
if (builtin) {res = l___regBuiltin_Int_reduceNeg_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1025_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}l___regBuiltin_Int_isPosValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1095____closed__1 = _init_l___regBuiltin_Int_isPosValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int___hyg_1095____closed__1();

185
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.c generated
View file

@ -102,6 +102,7 @@ static lean_object* l_Nat_reduceGE___closed__2;
static lean_object* l_Nat_reduceGcd___closed__1;
static lean_object* l___regBuiltin_Nat_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_1102____closed__6;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceGcd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_819_(lean_object*);
extern lean_object* l_Lean_Meta_Simp_builtinSimprocsRef;
static lean_object* l___regBuiltin_Nat_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_856____closed__4;
LEAN_EXPORT lean_object* l_Nat_reduceAdd(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Nat_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_1102____closed__4;
@ -112,6 +113,7 @@ LEAN_EXPORT lean_object* l_Nat_reduceLE___lambda__1___boxed(lean_object*, lean_o
static lean_object* l___regBuiltin_Nat_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_760____closed__6;
static lean_object* l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_570____closed__2;
lean_object* lean_nat_div(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
static lean_object* l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_570____closed__7;
static lean_object* l_Nat_reduceBinPred___lambda__1___closed__13;
LEAN_EXPORT lean_object* l_Nat_isValue___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -224,6 +226,7 @@ static lean_object* l___regBuiltin_Nat_reduceSub_declare____x40_Lean_Meta_Tactic
lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Nat_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_1102____closed__5;
lean_object* l_Lean_Meta_mkEqRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
static lean_object* l_Nat_reduceGcd___closed__2;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_724_(lean_object*);
static lean_object* l_Nat_reduceGT___closed__2;
@ -253,7 +256,6 @@ LEAN_EXPORT lean_object* l_Nat_reduceBin___lambda__1(lean_object*, lean_object*,
static lean_object* l___regBuiltin_Nat_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_646____closed__8;
static lean_object* l_Nat_reduceMul___closed__3;
static lean_object* l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_570____closed__6;
lean_object* l_Lean_Meta_Simp_addSimprocBuiltinAttr(lean_object*, uint8_t, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Nat_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_934____closed__1;
LEAN_EXPORT lean_object* l_Nat_isValue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Nat_reduceGE___closed__1;
@ -1969,15 +1971,24 @@ x_5 = l_Lean_Meta_Simp_registerBuiltinSimproc(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_Simp_builtinSimprocsRef;
return x_1;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_570____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_570____closed__7;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_570____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_570____closed__7;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reduceAdd___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -2413,12 +2424,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_610_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_608____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_608____closed__14;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_608____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceAdd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_608____closed__14;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reduceMul___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -2823,12 +2835,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_648_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_646____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_646____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_646____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceMul_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_646____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reduceSub___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -3233,12 +3246,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_686_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_684____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_684____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_684____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceSub_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_684____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reduceDiv___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -3643,12 +3657,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_724_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_722____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_722____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_722____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceDiv_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_722____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reduceMod___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -4053,12 +4068,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_762_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_760____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_760____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_760____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceMod_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_760____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reducePow___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -4463,12 +4479,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reducePow_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_800_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reducePow_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_798____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reducePow_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_798____closed__11;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reducePow_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_798____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reducePow_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_798____closed__11;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reduceGcd___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -4825,12 +4842,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceGcd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_819_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceGcd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_817____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceGcd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_817____closed__7;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceGcd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_817____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceGcd_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_817____closed__7;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reduceLT___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -5621,12 +5639,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_858_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_856____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_856____closed__10;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_856____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceLT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_856____closed__10;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reduceLE___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -6408,12 +6427,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_897_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_895____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_895____closed__9;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_895____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceLE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_895____closed__9;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reduceGT___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -7133,12 +7153,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_936_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_934____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_934____closed__3;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_934____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceGT_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_934____closed__3;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_reduceGE___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -7858,12 +7879,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_975_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_973____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_973____closed__3;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_973____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_reduceGE_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_973____closed__3;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Nat_isValue___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
@ -8107,12 +8129,13 @@ return x_5;
LEAN_EXPORT lean_object* l___regBuiltin_Nat_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_1104_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_2 = l___regBuiltin_Nat_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_1102____closed__2;
x_3 = 1;
x_4 = l___regBuiltin_Nat_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_1102____closed__9;
x_5 = l_Lean_Meta_Simp_addSimprocBuiltinAttr(x_2, x_3, x_4, x_1);
return x_5;
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1;
x_3 = l___regBuiltin_Nat_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_1102____closed__2;
x_4 = 1;
x_5 = l___regBuiltin_Nat_isValue_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_1102____closed__9;
x_6 = l_Lean_Meta_Simp_addSimprocBuiltinAttrCore(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
@ -8197,7 +8220,9 @@ lean_mark_persistent(l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tact
if (builtin) {res = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_570_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}if (builtin) {res = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572_(lean_io_mk_world());
}l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1 = _init_l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1();
lean_mark_persistent(l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572____closed__1);
if (builtin) {res = l___regBuiltin_Nat_reduceSucc_declare____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat___hyg_572_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
}l_Nat_reduceAdd___closed__1 = _init_l_Nat_reduceAdd___closed__1();

8442
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.c generated
View file

File diff suppressed because one or more lines are too long

34
stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c generated
View file

@ -29,7 +29,6 @@ lean_object* l_Lean_Meta_reduceRecMatcher_x3f(lean_object*, lean_object*, lean_o
static lean_object* l_Lean_Meta_Simp_simpLambda___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_lambdaTelescopeDSimp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_cacheResult___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_dsimp___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simpForall___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_dsimpGoal___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_dsimpGoal___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -343,7 +342,6 @@ lean_object* l_Lean_Meta_Simp_pre(lean_object*, lean_object*, lean_object*, lean
lean_object* l_Lean_Expr_forallE___override(lean_object*, lean_object*, lean_object*, uint8_t);
static lean_object* l_Lean_Meta_Simp_simpArrow___lambda__4___closed__9;
static lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_reduceStep___lambda__2___closed__2;
lean_object* l_Lean_Meta_DiscrTree_empty(lean_object*);
lean_object* l_Lean_Meta_Simp_getSimpCongrTheorems___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simpImpl_go___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
@ -377,7 +375,6 @@ lean_object* l_ST_Prim_Ref_modifyGetUnsafe___rarg___boxed(lean_object*, lean_obj
extern lean_object* l_Lean_levelZero;
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simpLet___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_simpForall___closed__1;
static lean_object* l_Lean_Meta_dsimp___closed__3;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_unfold_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_trySimpCongrTheorem_x3f___spec__1___closed__4;
lean_object* l_Lean_Expr_constName_x21(lean_object*);
@ -695,7 +692,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Sim
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simpLambda___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_dsimpImpl___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MVarId_assertHypotheses(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PersistentHashMap_empty___at_Lean_Meta_Instances_erased___default___spec__1;
LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_Simp_processCongrHypothesis___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isFVar(lean_object*);
lean_object* l_Lean_Expr_bindingInfo_x21(lean_object*);
@ -33801,30 +33797,8 @@ return x_24;
static lean_object* _init_l_Lean_Meta_dsimp___closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_DiscrTree_empty(lean_box(0));
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_dsimp___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_dsimp___closed__1;
x_2 = l_Lean_PersistentHashMap_empty___at_Lean_Meta_Instances_erased___default___spec__1;
x_3 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set(x_3, 2, x_2);
lean_ctor_set(x_3, 3, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_dsimp___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_dsimp___closed__2;
x_1 = l_Lean_Meta_Simp_lambdaTelescopeDSimp___rarg___closed__1;
x_2 = l_Lean_Meta_simp___closed__1;
x_3 = l_Lean_Meta_Simp_mkMethods(x_1, x_2);
return x_3;
@ -33836,7 +33810,7 @@ _start:
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = lean_ctor_get(x_6, 2);
lean_inc(x_9);
x_10 = l_Lean_Meta_dsimp___closed__3;
x_10 = l_Lean_Meta_dsimp___closed__1;
x_11 = lean_alloc_closure((void*)(l_Lean_Meta_Simp_dsimpMain), 9, 4);
lean_closure_set(x_11, 0, x_1);
lean_closure_set(x_11, 1, x_2);
@ -43733,10 +43707,6 @@ l_Lean_Meta_simp___closed__1 = _init_l_Lean_Meta_simp___closed__1();
lean_mark_persistent(l_Lean_Meta_simp___closed__1);
l_Lean_Meta_dsimp___closed__1 = _init_l_Lean_Meta_dsimp___closed__1();
lean_mark_persistent(l_Lean_Meta_dsimp___closed__1);
l_Lean_Meta_dsimp___closed__2 = _init_l_Lean_Meta_dsimp___closed__2();
lean_mark_persistent(l_Lean_Meta_dsimp___closed__2);
l_Lean_Meta_dsimp___closed__3 = _init_l_Lean_Meta_dsimp___closed__3();
lean_mark_persistent(l_Lean_Meta_dsimp___closed__3);
l_Lean_Meta_simpTargetCore___closed__1 = _init_l_Lean_Meta_simpTargetCore___closed__1();
lean_mark_persistent(l_Lean_Meta_simpTargetCore___closed__1);
l_Lean_Meta_simpTargetCore___closed__2 = _init_l_Lean_Meta_simpTargetCore___closed__2();

2626
stage0/stdlib/Lean/Meta/Tactic/Simp/RegisterCommand.c generated Normal file
View file

File diff suppressed because it is too large Load diff

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

@ -129,6 +129,7 @@ static lean_object* l___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simpArith___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_findSomeRevM_x3f_find___at_Lean_Meta_Simp_dischargeUsingAssumption_x3f___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_synthesizeArgs___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_userPostSimprocs___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_appArg_x21(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simpUsingDecide___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore___closed__3;
@ -212,7 +213,6 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_rewrite_x3f___s
LEAN_EXPORT lean_object* l_Lean_mkConstWithLevelParams___at_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_FVarId_getDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_dischargeDefault_x3f___lambda__1___closed__2;
lean_object* l_Lean_Meta_DiscrTree_empty(lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_rewrite_x3f___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___closed__11;
lean_object* l_Lean_Meta_getEqnsFor_x3f(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -259,7 +259,6 @@ static lean_object* l_Lean_isLevelMVarAssignable___at___private_Lean_Meta_Tactic
static lean_object* l_Lean_isLevelMVarAssignable___at___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___spec__5___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simpArith___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_userPostSimprocs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_Range_forIn_loop___at_Lean_Meta_Simp_SimprocEntry_try___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_simpUsingDecide___lambda__1___closed__12;
@ -273,18 +272,15 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simpGround___lambda__2(lean_object*, l
static lean_object* l_Lean_Meta_Simp_simpUsingDecide___lambda__1___closed__7;
lean_object* l_Lean_Meta_isRflTheorem(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_panic___at___private_Lean_Meta_WHNF_0__Lean_Meta_cached_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_userPreSimprocs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_appFn_x21(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_mkMethods___elambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_instMonadMetaM;
static lean_object* l_Lean_Meta_Simp_simpCtorEq___lambda__1___closed__4;
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simpGround___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_mkDefaultMethods___closed__4;
LEAN_EXPORT lean_object* l_Lean_MVarId_isAssignable___at___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_simpUsingDecide___lambda__1___closed__10;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simpMatchCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_postDefault___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_mkDefaultMethods___closed__3;
static lean_object* l___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___lambda__7___closed__1;
static lean_object* l___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_reduceOfNatNat___lambda__2___closed__2;
static lean_object* l_Lean_Meta_Simp_simpCtorEq___closed__2;
@ -394,6 +390,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Simp_simpUsingDecide(lean_object*, lean_obj
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_simpGround___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_rewritePre___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_tryTheoremWithExtraArgs_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Simp_userPreSimprocs___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_dischargeEqnThmHypothesis_x3f___closed__8;
lean_object* l_Lean_Expr_betaRev(lean_object*, lean_object*, uint8_t, uint8_t);
static lean_object* l_Lean_Meta_Simp_dischargeEqnThmHypothesis_x3f___closed__2;
@ -442,7 +439,6 @@ uint8_t l_Lean_Exception_isRuntime(lean_object*);
static lean_object* l_Lean_Meta_Simp_dischargeEqnThmHypothesis_x3f___closed__1;
static lean_object* l_Lean_Meta_Simp_simpUsingDecide___lambda__1___closed__16;
static lean_object* l_Lean_Meta_ppOrigin___at_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___spec__1___closed__1;
extern lean_object* l_Lean_PersistentHashMap_empty___at_Lean_Meta_Instances_erased___default___spec__1;
static lean_object* l_Lean_Meta_Simp_mkDefaultMethods___closed__2;
static lean_object* l_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___closed__14;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_rewritePost___spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -17147,7 +17143,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Simp_preDefault___lambda__1(lean_object* x_
_start:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_12 = lean_alloc_closure((void*)(l_Lean_Meta_Simp_userPreSimprocs), 10, 1);
x_12 = lean_alloc_closure((void*)(l_Lean_Meta_Simp_userPreSimprocs___boxed), 10, 1);
lean_closure_set(x_12, 0, x_1);
x_13 = l_Lean_Meta_Simp_preDefault___lambda__1___closed__1;
x_14 = lean_alloc_closure((void*)(l_Lean_Meta_Simp_andThen), 11, 2);
@ -17253,7 +17249,7 @@ lean_inc(x_2);
x_14 = lean_alloc_closure((void*)(l_Lean_Meta_Simp_rewritePost___boxed), 11, 2);
lean_closure_set(x_14, 0, x_2);
lean_closure_set(x_14, 1, x_13);
x_15 = lean_alloc_closure((void*)(l_Lean_Meta_Simp_userPostSimprocs), 10, 1);
x_15 = lean_alloc_closure((void*)(l_Lean_Meta_Simp_userPostSimprocs___boxed), 10, 1);
lean_closure_set(x_15, 0, x_1);
x_16 = lean_alloc_closure((void*)(l_Lean_Meta_Simp_postDefault___lambda__3), 11, 2);
lean_closure_set(x_16, 0, x_2);
@ -20361,30 +20357,8 @@ return x_1;
static lean_object* _init_l_Lean_Meta_Simp_mkDefaultMethods___closed__2() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_DiscrTree_empty(lean_box(0));
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Simp_mkDefaultMethods___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Simp_mkDefaultMethods___closed__2;
x_2 = l_Lean_PersistentHashMap_empty___at_Lean_Meta_Instances_erased___default___spec__1;
x_3 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set(x_3, 2, x_2);
lean_ctor_set(x_3, 3, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Simp_mkDefaultMethods___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Simp_mkDefaultMethods___closed__3;
x_1 = l___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore___closed__1;
x_2 = l_Lean_Meta_Simp_mkDefaultMethodsCore___closed__1;
x_3 = l_Lean_Meta_Simp_mkMethods(x_1, x_2);
return x_3;
@ -20400,7 +20374,7 @@ x_6 = l_Lean_Option_get___at___private_Lean_Util_Profile_0__Lean_get__profiler__
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8;
x_7 = l_Lean_Meta_Simp_mkDefaultMethods___closed__4;
x_7 = l_Lean_Meta_Simp_mkDefaultMethods___closed__2;
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_3);
@ -20413,27 +20387,31 @@ x_9 = l_Lean_Meta_Simp_getSimprocs___rarg(x_2, x_3);
x_10 = !lean_is_exclusive(x_9);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_11 = lean_ctor_get(x_9, 0);
x_12 = l_Lean_Meta_Simp_mkDefaultMethodsCore___closed__1;
x_13 = l_Lean_Meta_Simp_mkMethods(x_11, x_12);
lean_ctor_set(x_9, 0, x_13);
x_12 = l_Lean_Meta_Simp_simpCtorEq___lambda__1___closed__4;
x_13 = lean_array_push(x_12, x_11);
x_14 = l_Lean_Meta_Simp_mkDefaultMethodsCore___closed__1;
x_15 = l_Lean_Meta_Simp_mkMethods(x_13, x_14);
lean_ctor_set(x_9, 0, x_15);
return x_9;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_14 = lean_ctor_get(x_9, 0);
x_15 = lean_ctor_get(x_9, 1);
lean_inc(x_15);
lean_inc(x_14);
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_16 = lean_ctor_get(x_9, 0);
x_17 = lean_ctor_get(x_9, 1);
lean_inc(x_17);
lean_inc(x_16);
lean_dec(x_9);
x_16 = l_Lean_Meta_Simp_mkDefaultMethodsCore___closed__1;
x_17 = l_Lean_Meta_Simp_mkMethods(x_14, x_16);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_15);
return x_18;
x_18 = l_Lean_Meta_Simp_simpCtorEq___lambda__1___closed__4;
x_19 = lean_array_push(x_18, x_16);
x_20 = l_Lean_Meta_Simp_mkDefaultMethodsCore___closed__1;
x_21 = l_Lean_Meta_Simp_mkMethods(x_19, x_20);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_17);
return x_22;
}
}
}
@ -20771,10 +20749,6 @@ l_Lean_Meta_Simp_mkDefaultMethods___closed__1 = _init_l_Lean_Meta_Simp_mkDefault
lean_mark_persistent(l_Lean_Meta_Simp_mkDefaultMethods___closed__1);
l_Lean_Meta_Simp_mkDefaultMethods___closed__2 = _init_l_Lean_Meta_Simp_mkDefaultMethods___closed__2();
lean_mark_persistent(l_Lean_Meta_Simp_mkDefaultMethods___closed__2);
l_Lean_Meta_Simp_mkDefaultMethods___closed__3 = _init_l_Lean_Meta_Simp_mkDefaultMethods___closed__3();
lean_mark_persistent(l_Lean_Meta_Simp_mkDefaultMethods___closed__3);
l_Lean_Meta_Simp_mkDefaultMethods___closed__4 = _init_l_Lean_Meta_Simp_mkDefaultMethods___closed__4();
lean_mark_persistent(l_Lean_Meta_Simp_mkDefaultMethods___closed__4);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

1962
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c generated
View file

File diff suppressed because it is too large Load diff

8683
stage0/stdlib/Lean/Meta/Tactic/Simp/Simproc.c generated
View file

File diff suppressed because it is too large Load diff

13
stage0/stdlib/Lean/Meta/Tactic/SplitIf.c generated
View file

@ -3818,15 +3818,10 @@ return x_10;
static lean_object* _init_l_Lean_Meta_simpIfTarget___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_SplitIf_initFn____x40_Lean_Meta_Tactic_SplitIf___hyg_5____closed__1;
x_2 = l_Lean_PersistentHashMap_empty___at_Lean_Meta_Instances_erased___default___spec__1;
x_3 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set(x_3, 2, x_2);
lean_ctor_set(x_3, 3, x_2);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_simpIfTarget___closed__2() {