chore: update stage0
This commit is contained in:
Leonardo de Moura
Sebastian Ullrich
parent
ad58deeae3
commit
88801166b6
12 changed files with 79665 additions and 2484 deletions
10
stage0/stdlib/Init/Data/Fin/Basic.c
generated
10
stage0/stdlib/Init/Data/Fin/Basic.c
generated
|
|
@ -19,7 +19,6 @@ LEAN_EXPORT lean_object* l_instGetElemFinVal___rarg(lean_object*, lean_object*,
|
|||
LEAN_EXPORT lean_object* l_Fin_instXorFin(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Fin_succ___boxed(lean_object*);
|
||||
static lean_object* l___aux__Init__Data__Fin__Basic______macroRules__tacticGet__elem__tactic__trivial__1___closed__13;
|
||||
LEAN_EXPORT lean_object* l_Fin_instOfNatFinHAddNatInstHAddInstAddNatOfNat___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Fin_div___boxed(lean_object*);
|
||||
static lean_object* l___aux__Init__Data__Fin__Basic______macroRules__tacticGet__elem__tactic__trivial__1___closed__10;
|
||||
LEAN_EXPORT lean_object* l_Fin_ofNat_x27(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -36,12 +35,14 @@ LEAN_EXPORT lean_object* l_Fin_div(lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Fin_coeToNat___boxed(lean_object*);
|
||||
static lean_object* l___aux__Init__Data__Fin__Basic______macroRules__tacticGet__elem__tactic__trivial__1___closed__17;
|
||||
static lean_object* l___aux__Init__Data__Fin__Basic______macroRules__tacticGet__elem__tactic__trivial__1___closed__7;
|
||||
LEAN_EXPORT lean_object* l_Fin_ofNatInst(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_node5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Fin_instInhabitedFinHAddNatInstHAddInstAddNatOfNat___boxed(lean_object*);
|
||||
lean_object* lean_nat_shiftr(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Fin_add(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Fin_instDivFin(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Fin_ofNatInst___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Fin_ofNat(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Fin_ofNat_x27___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___aux__Init__Data__Fin__Basic______macroRules__tacticGet__elem__tactic__trivial__1___closed__19;
|
||||
|
|
@ -98,7 +99,6 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Fin_modn(lean_object*);
|
||||
lean_object* lean_nat_mul(lean_object*, lean_object*);
|
||||
static lean_object* l___aux__Init__Data__Fin__Basic______macroRules__tacticGet__elem__tactic__trivial__1___closed__15;
|
||||
LEAN_EXPORT lean_object* l_Fin_instOfNatFinHAddNatInstHAddInstAddNatOfNat(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Fin_lor(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Fin_mod(lean_object*);
|
||||
static lean_object* l___aux__Init__Data__Fin__Basic______macroRules__tacticGet__elem__tactic__trivial__1___closed__22;
|
||||
|
|
@ -638,7 +638,7 @@ lean_closure_set(x_2, 0, x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Fin_instOfNatFinHAddNatInstHAddInstAddNatOfNat(lean_object* x_1, lean_object* x_2) {
|
||||
LEAN_EXPORT lean_object* l_Fin_ofNatInst(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
|
|
@ -646,11 +646,11 @@ x_3 = l_Fin_ofNat(x_1, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Fin_instOfNatFinHAddNatInstHAddInstAddNatOfNat___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
LEAN_EXPORT lean_object* l_Fin_ofNatInst___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Fin_instOfNatFinHAddNatInstHAddInstAddNatOfNat(x_1, x_2);
|
||||
x_3 = l_Fin_ofNatInst(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
|
|
|
|||
4
stage0/stdlib/Init/Data/Int/Basic.c
generated
4
stage0/stdlib/Init/Data/Int/Basic.c
generated
|
|
@ -15,7 +15,6 @@ extern "C" {
|
|||
#endif
|
||||
uint8_t lean_int_dec_nonneg(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instCoeNatInt(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instOfNatInt(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Int_add___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Int_instMinInt___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Int_mod___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -30,6 +29,7 @@ LEAN_EXPORT lean_object* l_Int_instNegInt;
|
|||
LEAN_EXPORT lean_object* l_Int_instMaxInt___boxed(lean_object*, lean_object*);
|
||||
lean_object* lean_nat_to_int(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Int_pow(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_ofNatInst(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Int_instDecidableEqInt___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Int_decLe___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Int_decLt___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -100,7 +100,7 @@ x_2 = lean_nat_to_int(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_instOfNatInt(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_ofNatInst(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
|
|
|
|||
50
stage0/stdlib/Init/Data/UInt/Basic.c
generated
50
stage0/stdlib/Init/Data/UInt/Basic.c
generated
|
|
@ -15,6 +15,7 @@ extern "C" {
|
|||
#endif
|
||||
LEAN_EXPORT lean_object* l_UInt64_modn___boxed(lean_object*, lean_object*);
|
||||
uint8_t lean_uint8_sub(uint8_t, uint8_t);
|
||||
LEAN_EXPORT lean_object* l_UInt32_ofNatInst___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instComplementUInt32;
|
||||
LEAN_EXPORT lean_object* l_USize_mul___boxed(lean_object*, lean_object*);
|
||||
uint8_t lean_uint32_to_uint8(uint32_t);
|
||||
|
|
@ -24,7 +25,6 @@ LEAN_EXPORT lean_object* l_instModUInt16;
|
|||
uint16_t lean_uint64_to_uint16(uint64_t);
|
||||
LEAN_EXPORT lean_object* l_USize_lor___boxed(lean_object*, lean_object*);
|
||||
size_t lean_usize_shift_right(size_t, size_t);
|
||||
LEAN_EXPORT lean_object* l_instOfNatUInt16___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instMulUInt64;
|
||||
LEAN_EXPORT lean_object* l_instDecidableLeUInt16InstLEUInt16___boxed(lean_object*, lean_object*);
|
||||
uint8_t lean_uint8_lor(uint8_t, uint8_t);
|
||||
|
|
@ -68,6 +68,7 @@ static lean_object* l_instAddUInt8___closed__1;
|
|||
uint32_t lean_uint32_shift_right(uint32_t, uint32_t);
|
||||
uint8_t lean_uint64_dec_lt(uint64_t, uint64_t);
|
||||
static lean_object* l_instDivUSize___closed__1;
|
||||
LEAN_EXPORT uint8_t l_UInt8_ofNatInst(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_USize_div___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Nat_toUInt16___boxed(lean_object*);
|
||||
static lean_object* l_instShiftRightUInt8___closed__1;
|
||||
|
|
@ -76,7 +77,6 @@ LEAN_EXPORT uint16_t l_instMaxUInt16(uint16_t, uint16_t);
|
|||
uint16_t lean_uint16_complement(uint16_t);
|
||||
LEAN_EXPORT lean_object* l_instOrOpUSize;
|
||||
LEAN_EXPORT lean_object* l_UInt8_lor___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instOfNatUInt64___boxed(lean_object*);
|
||||
uint8_t lean_uint8_land(uint8_t, uint8_t);
|
||||
LEAN_EXPORT lean_object* l_UInt64_mul___boxed(lean_object*, lean_object*);
|
||||
static lean_object* l_instModUInt8___closed__1;
|
||||
|
|
@ -120,6 +120,7 @@ size_t lean_usize_of_nat(lean_object*);
|
|||
static lean_object* l_instMulUSize___closed__1;
|
||||
LEAN_EXPORT lean_object* l_UInt8_ofNat___boxed(lean_object*);
|
||||
uint32_t lean_uint32_mul(uint32_t, uint32_t);
|
||||
LEAN_EXPORT size_t l_USize_ofNatInst(lean_object*);
|
||||
size_t lean_usize_modn(size_t, lean_object*);
|
||||
size_t lean_usize_lor(size_t, size_t);
|
||||
static lean_object* l_instAndOpUInt32___closed__1;
|
||||
|
|
@ -134,7 +135,6 @@ uint64_t lean_uint64_shift_right(uint64_t, uint64_t);
|
|||
LEAN_EXPORT lean_object* l_USize_complement___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt32_toUSize___boxed(lean_object*);
|
||||
uint64_t lean_uint64_complement(uint64_t);
|
||||
LEAN_EXPORT lean_object* l_instOfNatUSize___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instDivUInt64;
|
||||
uint32_t lean_uint32_of_nat(lean_object*);
|
||||
uint16_t lean_uint16_xor(uint16_t, uint16_t);
|
||||
|
|
@ -171,6 +171,7 @@ LEAN_EXPORT lean_object* l_instMulUSize;
|
|||
uint16_t lean_uint8_to_uint16(uint8_t);
|
||||
LEAN_EXPORT lean_object* l_UInt8_land___boxed(lean_object*, lean_object*);
|
||||
uint64_t lean_uint64_div(uint64_t, uint64_t);
|
||||
LEAN_EXPORT lean_object* l_UInt8_ofNatInst___boxed(lean_object*);
|
||||
static lean_object* l_instShiftRightUSize___closed__1;
|
||||
LEAN_EXPORT lean_object* l_instMinUInt8___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt64_toUInt16___boxed(lean_object*);
|
||||
|
|
@ -196,7 +197,6 @@ uint32_t lean_uint32_xor(uint32_t, uint32_t);
|
|||
uint8_t lean_uint16_to_uint8(uint16_t);
|
||||
LEAN_EXPORT lean_object* l_UInt16_shiftLeft___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_USize_mod___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instOfNatUInt32___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Nat_toUInt32___boxed(lean_object*);
|
||||
uint8_t lean_uint8_div(uint8_t, uint8_t);
|
||||
LEAN_EXPORT lean_object* l_instMaxUInt16___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -220,10 +220,12 @@ LEAN_EXPORT lean_object* l_instOrOpUInt32;
|
|||
uint8_t lean_uint8_complement(uint8_t);
|
||||
LEAN_EXPORT lean_object* l_UInt64_mod___boxed(lean_object*, lean_object*);
|
||||
static lean_object* l_instOrOpUInt8___closed__1;
|
||||
LEAN_EXPORT uint16_t l_UInt16_ofNatInst(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instSubUInt64;
|
||||
LEAN_EXPORT lean_object* l_UInt8_xor___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instOrOpUInt16;
|
||||
uint32_t lean_uint32_modn(uint32_t, lean_object*);
|
||||
LEAN_EXPORT uint32_t l_UInt32_ofNatInst(lean_object*);
|
||||
LEAN_EXPORT uint8_t l_instDecidableLeUInt16InstLEUInt16(uint16_t, uint16_t);
|
||||
static lean_object* l_instComplementUInt64___closed__1;
|
||||
static lean_object* l_instHModUInt8Nat___closed__1;
|
||||
|
|
@ -236,6 +238,7 @@ LEAN_EXPORT lean_object* l_instLTUSize;
|
|||
uint32_t lean_uint32_sub(uint32_t, uint32_t);
|
||||
static lean_object* l_instModUInt16___closed__1;
|
||||
LEAN_EXPORT lean_object* l_UInt16_toUInt64___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt64_ofNatInst___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instShiftRightUSize;
|
||||
uint16_t lean_uint16_lor(uint16_t, uint16_t);
|
||||
LEAN_EXPORT lean_object* l_instDivUInt16;
|
||||
|
|
@ -244,6 +247,7 @@ uint64_t lean_uint16_to_uint64(uint16_t);
|
|||
LEAN_EXPORT uint64_t l_instMaxUInt64(uint64_t, uint64_t);
|
||||
LEAN_EXPORT lean_object* l_UInt16_decLt___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_USize_land___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT uint64_t l_UInt64_ofNatInst(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt16_toUInt8___boxed(lean_object*);
|
||||
uint16_t lean_uint16_add(uint16_t, uint16_t);
|
||||
uint32_t lean_uint32_of_nat(lean_object*);
|
||||
|
|
@ -251,7 +255,6 @@ LEAN_EXPORT lean_object* l_instOrOpUInt64;
|
|||
static lean_object* l_instAndOpUInt16___closed__1;
|
||||
LEAN_EXPORT lean_object* l_instDecidableLtUInt16InstLTUInt16___boxed(lean_object*, lean_object*);
|
||||
static lean_object* l_instMulUInt8___closed__1;
|
||||
LEAN_EXPORT uint8_t l_instOfNatUInt8(lean_object*);
|
||||
LEAN_EXPORT uint64_t l_Nat_toUInt64(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt64_toUInt32___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt16_div___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -260,10 +263,8 @@ LEAN_EXPORT lean_object* l_instMulUInt8;
|
|||
LEAN_EXPORT lean_object* l_instShiftLeftUInt64;
|
||||
LEAN_EXPORT lean_object* l_UInt16_shiftRight___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt32_xor___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instOfNatUInt8___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt32_mod___boxed(lean_object*, lean_object*);
|
||||
uint8_t lean_uint8_xor(uint8_t, uint8_t);
|
||||
LEAN_EXPORT uint32_t l_instOfNatUInt32(lean_object*);
|
||||
static lean_object* l_instComplementUInt8___closed__1;
|
||||
static lean_object* l_instComplementUSize___closed__1;
|
||||
LEAN_EXPORT lean_object* l_instHModUInt8Nat;
|
||||
|
|
@ -291,10 +292,10 @@ uint8_t lean_uint8_dec_le(uint8_t, uint8_t);
|
|||
uint64_t lean_uint64_shift_left(uint64_t, uint64_t);
|
||||
static lean_object* l_instShiftLeftUInt8___closed__1;
|
||||
LEAN_EXPORT lean_object* l_USize_sub___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT uint16_t l_instOfNatUInt16(lean_object*);
|
||||
uint8_t lean_uint8_shift_right(uint8_t, uint8_t);
|
||||
LEAN_EXPORT lean_object* l_USize_shiftLeft___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instMinUSize___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt16_ofNatInst___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt32_ofNat_x27___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instMinUInt64___boxed(lean_object*, lean_object*);
|
||||
uint8_t lean_uint8_of_nat(lean_object*);
|
||||
|
|
@ -308,7 +309,6 @@ LEAN_EXPORT lean_object* l_instDecidableLeUInt8InstLEUInt8___boxed(lean_object*,
|
|||
LEAN_EXPORT lean_object* l_instSubUInt16;
|
||||
size_t lean_usize_sub(size_t, size_t);
|
||||
LEAN_EXPORT uint16_t l_instMinUInt16(uint16_t, uint16_t);
|
||||
LEAN_EXPORT size_t l_instOfNatUSize(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt64_xor___boxed(lean_object*, lean_object*);
|
||||
uint16_t lean_uint16_modn(uint16_t, lean_object*);
|
||||
lean_object* lean_uint8_to_nat(uint8_t);
|
||||
|
|
@ -339,7 +339,6 @@ LEAN_EXPORT lean_object* l_instAndOpUInt8;
|
|||
static lean_object* l_instSubUInt16___closed__1;
|
||||
static lean_object* l_instOrOpUSize___closed__1;
|
||||
uint64_t lean_uint64_modn(uint64_t, lean_object*);
|
||||
LEAN_EXPORT uint64_t l_instOfNatUInt64(lean_object*);
|
||||
static lean_object* l_instModUInt64___closed__1;
|
||||
LEAN_EXPORT lean_object* l_USize_toUInt32___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_USize_add___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -353,6 +352,7 @@ uint16_t lean_uint16_mul(uint16_t, uint16_t);
|
|||
LEAN_EXPORT lean_object* l_instDivUInt8;
|
||||
uint8_t lean_usize_dec_lt(size_t, size_t);
|
||||
LEAN_EXPORT lean_object* l_UInt16_decLe___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_USize_ofNatInst___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt32_modn___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_UInt16_complement___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_instDivUInt32;
|
||||
|
|
@ -559,7 +559,7 @@ x_6 = lean_box(x_5);
|
|||
return x_6;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT uint8_t l_instOfNatUInt8(lean_object* x_1) {
|
||||
LEAN_EXPORT uint8_t l_UInt8_ofNatInst(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_2;
|
||||
|
|
@ -567,11 +567,11 @@ x_2 = lean_uint8_of_nat(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_instOfNatUInt8___boxed(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_UInt8_ofNatInst___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_2; lean_object* x_3;
|
||||
x_2 = l_instOfNatUInt8(x_1);
|
||||
x_2 = l_UInt8_ofNatInst(x_1);
|
||||
lean_dec(x_1);
|
||||
x_3 = lean_box(x_2);
|
||||
return x_3;
|
||||
|
|
@ -1122,7 +1122,7 @@ x_6 = lean_box(x_5);
|
|||
return x_6;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT uint16_t l_instOfNatUInt16(lean_object* x_1) {
|
||||
LEAN_EXPORT uint16_t l_UInt16_ofNatInst(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint16_t x_2;
|
||||
|
|
@ -1130,11 +1130,11 @@ x_2 = lean_uint16_of_nat(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_instOfNatUInt16___boxed(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_UInt16_ofNatInst___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint16_t x_2; lean_object* x_3;
|
||||
x_2 = l_instOfNatUInt16(x_1);
|
||||
x_2 = l_UInt16_ofNatInst(x_1);
|
||||
lean_dec(x_1);
|
||||
x_3 = lean_box(x_2);
|
||||
return x_3;
|
||||
|
|
@ -1706,7 +1706,7 @@ x_4 = lean_box_uint32(x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT uint32_t l_instOfNatUInt32(lean_object* x_1) {
|
||||
LEAN_EXPORT uint32_t l_UInt32_ofNatInst(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint32_t x_2;
|
||||
|
|
@ -1714,11 +1714,11 @@ x_2 = lean_uint32_of_nat(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_instOfNatUInt32___boxed(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_UInt32_ofNatInst___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint32_t x_2; lean_object* x_3;
|
||||
x_2 = l_instOfNatUInt32(x_1);
|
||||
x_2 = l_UInt32_ofNatInst(x_1);
|
||||
lean_dec(x_1);
|
||||
x_3 = lean_box_uint32(x_2);
|
||||
return x_3;
|
||||
|
|
@ -2173,7 +2173,7 @@ x_4 = lean_box_uint64(x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT uint64_t l_instOfNatUInt64(lean_object* x_1) {
|
||||
LEAN_EXPORT uint64_t l_UInt64_ofNatInst(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint64_t x_2;
|
||||
|
|
@ -2181,11 +2181,11 @@ x_2 = lean_uint64_of_nat(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_instOfNatUInt64___boxed(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_UInt64_ofNatInst___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
uint64_t x_2; lean_object* x_3;
|
||||
x_2 = l_instOfNatUInt64(x_1);
|
||||
x_2 = l_UInt64_ofNatInst(x_1);
|
||||
lean_dec(x_1);
|
||||
x_3 = lean_box_uint64(x_2);
|
||||
return x_3;
|
||||
|
|
@ -2747,7 +2747,7 @@ x_4 = lean_box_uint32(x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT size_t l_instOfNatUSize(lean_object* x_1) {
|
||||
LEAN_EXPORT size_t l_USize_ofNatInst(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
size_t x_2;
|
||||
|
|
@ -2755,11 +2755,11 @@ x_2 = lean_usize_of_nat(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_instOfNatUSize___boxed(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_USize_ofNatInst___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
size_t x_2; lean_object* x_3;
|
||||
x_2 = l_instOfNatUSize(x_1);
|
||||
x_2 = l_USize_ofNatInst(x_1);
|
||||
lean_dec(x_1);
|
||||
x_3 = lean_box_usize(x_2);
|
||||
return x_3;
|
||||
|
|
|
|||
280
stage0/stdlib/Lean/Elab/Tactic/Simp.c
generated
280
stage0/stdlib/Lean/Elab/Tactic/Simp.c
generated
|
|
@ -24,6 +24,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDSimp___closed__3;
|
|||
lean_object* lean_format_pretty(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDSimp(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_mkSimpOnly___lambda__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_dsimpLocation_go(lean_object*, lean_object*, uint8_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_Elab_Tactic_Simp_DischargeWrapper_with___rarg___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_Elab_Tactic_evalUnsafe____x40_Lean_Elab_Tactic_Simp___hyg_184____boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -47,6 +48,7 @@ static lean_object* l_Lean_Elab_Tactic_tacticToDischarge___closed__8;
|
|||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_elabSimpConfigCore___spec__6(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Meta_SimpTheoremsArray_isErased(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_mkSimpOnly___spec__11(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__6;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabSimpConfigCtxCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_dsimpLocation_go___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_EXPORT lean_object* l_Lean_Elab_Tactic_tactic_simp_trace;
|
||||
|
|
@ -62,7 +64,9 @@ lean_object* l_Lean_LocalContext_findFromUserName_x3f(lean_object*, lean_object*
|
|||
lean_object* l_List_mapTR_loop___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
|
||||
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_elabSimpArgs___spec__16___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_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__4;
|
||||
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__2;
|
||||
lean_object* l_Lean_Syntax_formatStxAux(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
uint8_t l_List_elem___at_Lean_NameHashSet_insert___spec__2(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -132,10 +136,8 @@ static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_ela
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabSimpArgs___lambda__2___boxed(lean_object**);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabSimpArgs_resolveSimpIdTheorem_x3f___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_Elab_Tactic_elabDSimpConfigCore___closed__3;
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__6;
|
||||
LEAN_EXPORT lean_object* l_Lean_HashMap_toArray___at_Lean_Elab_Tactic_mkSimpOnly___spec__1(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabSimpArgs_isSimproc_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabSimpConfig(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_LocalContext_empty;
|
||||
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDSimp_declRange___closed__4;
|
||||
|
|
@ -199,7 +201,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDSimp___closed__5;
|
|||
lean_object* l_Lean_Meta_SimpTheorems_add(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalDSimp(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_getNondepPropHyps(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__5;
|
||||
static lean_object* l_Lean_Elab_Tactic_tacticToDischarge___closed__14;
|
||||
lean_object* l_List_mapTR_loop___at_Lean_resolveGlobalConstCore___spec__2(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentArray_mapMAux___at_Lean_Elab_Tactic_elabSimpConfigCore___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -264,7 +265,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabSimpArgs_isSimproc_x3f___lambda_
|
|||
LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_elabSimpArgs___spec__8(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*);
|
||||
static lean_object* l_Lean_Elab_Tactic_mkSimpOnly___lambda__2___closed__3;
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__2;
|
||||
static lean_object* l_Lean_Elab_Tactic_mkSimpContext___lambda__3___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabSimpConfigCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_List_isEmpty___rarg(lean_object*);
|
||||
|
|
@ -288,6 +288,7 @@ static lean_object* l_Lean_Elab_Tactic_simpOnlyBuiltins___closed__4;
|
|||
lean_object* l_Lean_Syntax_mkSep(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_Simp_isSimproc(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_mkSimpOnly___lambda__1___closed__8;
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__7;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabSimpConfig___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_mkSimpContext___lambda__2(lean_object*, uint8_t, uint8_t, lean_object*, uint8_t, uint8_t, 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_Elab_Tactic_mkSimpOnly___spec__10___lambda__2___closed__3;
|
||||
|
|
@ -319,6 +320,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Tactic_elabSimp
|
|||
LEAN_EXPORT lean_object* l_Lean_unresolveNameGlobal_unresolveNameCore___at_Lean_Elab_Tactic_mkSimpOnly___spec__6___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_componentsRev(lean_object*);
|
||||
static lean_object* l_Array_qsort_sort___at_Lean_Elab_Tactic_mkSimpOnly___spec__4___closed__1;
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__1;
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_rootNamespace;
|
||||
|
|
@ -364,6 +366,7 @@ LEAN_EXPORT lean_object* l_Lean_unresolveNameGlobal___at_Lean_Elab_Tactic_mkSimp
|
|||
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange___closed__4;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___at_Lean_Elab_Tactic_elabSimpArgs___spec__3___lambda__1(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_Elab_Tactic_mkSimpOnly___spec__10___closed__2;
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__5;
|
||||
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_tacticToDischarge___closed__12;
|
||||
|
|
@ -388,7 +391,6 @@ lean_object* l_Lean_Name_mkStr6(lean_object*, lean_object*, lean_object*, lean_o
|
|||
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_elabSimpArgs___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Tactic_saveState___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_evalUnsafe____x40_Lean_Elab_Tactic_Simp___hyg_7____closed__5;
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__3;
|
||||
static lean_object* l_Lean_Meta_SimpTheorems_erase___at_Lean_Elab_Tactic_elabSimpArgs___spec__19___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_PersistentArray_mapM___at_Lean_Elab_Tactic_elabSimpConfigCore___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -410,11 +412,11 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_dsimpLocation___lambda__2___boxed(le
|
|||
static lean_object* l_Lean_Elab_Tactic_elabSimpConfigCore___closed__11;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalSimpAll___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*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_mkSimpOnly___spec__10___lambda__2___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_AssocList_foldlM___at_Lean_Elab_Tactic_mkSimpOnly___spec__2___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_traceSimpCall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalSimpAll___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*);
|
||||
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange(lean_object*);
|
||||
lean_object* l_Lean_Meta_Simp_isBuiltinSimproc(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_tacticToDischarge___closed__3;
|
||||
lean_object* l_Lean_Meta_SimpTheorems_addLetDeclToUnfold(lean_object*, lean_object*);
|
||||
|
|
@ -424,7 +426,6 @@ lean_object* l_Lean_Elab_Term_TermElabM_run___rarg(lean_object*, lean_object*, l
|
|||
LEAN_EXPORT lean_object* l_Lean_PersistentArray_mapM___at_Lean_Elab_Tactic_elabSimpConfigCore___spec__7(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_Elab_Tactic_mkSimpContext___spec__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_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_mkSimpOnly___spec__8___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*);
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__7;
|
||||
lean_object* l_Lean_Meta_withLCtx___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___spec__3___rarg(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_mkStr2(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Meta_instInhabitedSimpTheorems;
|
||||
|
|
@ -465,7 +466,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tacti
|
|||
LEAN_EXPORT lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_elabSimpArgs___spec__10___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_mapMUnsafe_map___at_Lean_Elab_Tactic_elabSimpConfigCore___spec__6___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_resolveGlobalConst___at_Lean_Elab_Tactic_elabSimpArgs___spec__5___closed__3;
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__4;
|
||||
lean_object* l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_elabSimpConfigCore___spec__5___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_Elab_Tactic_simpOnlyBuiltins___closed__5;
|
||||
|
|
@ -493,6 +493,7 @@ extern lean_object* l_Lean_Meta_Simp_defaultMaxSteps;
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_addConstInfo___at_Lean_Elab_Tactic_elabSimpArgs___spec__13(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_Elab_Tactic_SimpKind_noConfusion___rarg___closed__1;
|
||||
lean_object* lean_array_uget(lean_object*, size_t);
|
||||
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__3;
|
||||
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__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_Lean_Elab_Tactic_elabSimpConfigCtxCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_mkSimpContext___lambda__2___closed__2;
|
||||
|
|
@ -5174,9 +5175,7 @@ x_79 = lean_ctor_get(x_78, 0);
|
|||
lean_inc(x_79);
|
||||
if (lean_obj_tag(x_79) == 0)
|
||||
{
|
||||
lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84;
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_8);
|
||||
lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; uint8_t x_85;
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
x_80 = lean_ctor_get(x_78, 1);
|
||||
|
|
@ -5185,62 +5184,62 @@ lean_dec(x_78);
|
|||
x_81 = l_Lean_Syntax_getId(x_1);
|
||||
lean_dec(x_1);
|
||||
x_82 = lean_erase_macro_scopes(x_81);
|
||||
x_83 = l_Lean_Meta_getSimpExtension_x3f(x_82, x_80);
|
||||
lean_inc(x_82);
|
||||
x_83 = l_Lean_Meta_Simp_isBuiltinSimproc(x_82, x_8, x_9, x_80);
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_8);
|
||||
x_84 = lean_ctor_get(x_83, 0);
|
||||
lean_inc(x_84);
|
||||
if (lean_obj_tag(x_84) == 0)
|
||||
{
|
||||
lean_object* x_85; lean_object* x_86;
|
||||
x_85 = lean_ctor_get(x_83, 1);
|
||||
lean_inc(x_85);
|
||||
lean_dec(x_83);
|
||||
x_86 = l_Lean_Elab_Tactic_elabSimpArgs_resolveSimpIdTheorem_x3f___closed__3;
|
||||
x_11 = x_86;
|
||||
x_12 = x_85;
|
||||
goto block_15;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91;
|
||||
x_87 = lean_ctor_get(x_83, 1);
|
||||
lean_inc(x_87);
|
||||
lean_dec(x_83);
|
||||
x_88 = lean_ctor_get(x_84, 0);
|
||||
lean_inc(x_88);
|
||||
x_85 = lean_unbox(x_84);
|
||||
lean_dec(x_84);
|
||||
x_89 = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(x_89, 0, x_88);
|
||||
x_90 = lean_box(0);
|
||||
x_91 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_91, 0, x_89);
|
||||
lean_ctor_set(x_91, 1, x_90);
|
||||
x_11 = x_91;
|
||||
x_12 = x_87;
|
||||
if (x_85 == 0)
|
||||
{
|
||||
lean_object* x_86; lean_object* x_87; lean_object* x_88;
|
||||
x_86 = lean_ctor_get(x_83, 1);
|
||||
lean_inc(x_86);
|
||||
lean_dec(x_83);
|
||||
x_87 = l_Lean_Meta_getSimpExtension_x3f(x_82, x_86);
|
||||
x_88 = lean_ctor_get(x_87, 0);
|
||||
lean_inc(x_88);
|
||||
if (lean_obj_tag(x_88) == 0)
|
||||
{
|
||||
lean_object* x_89; lean_object* x_90;
|
||||
x_89 = lean_ctor_get(x_87, 1);
|
||||
lean_inc(x_89);
|
||||
lean_dec(x_87);
|
||||
x_90 = l_Lean_Elab_Tactic_elabSimpArgs_resolveSimpIdTheorem_x3f___closed__3;
|
||||
x_11 = x_90;
|
||||
x_12 = x_89;
|
||||
goto block_15;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95;
|
||||
x_91 = lean_ctor_get(x_87, 1);
|
||||
lean_inc(x_91);
|
||||
lean_dec(x_87);
|
||||
x_92 = lean_ctor_get(x_88, 0);
|
||||
lean_inc(x_92);
|
||||
lean_dec(x_88);
|
||||
x_93 = lean_alloc_ctor(3, 1, 0);
|
||||
lean_ctor_set(x_93, 0, x_92);
|
||||
x_94 = lean_box(0);
|
||||
x_95 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_95, 0, x_93);
|
||||
lean_ctor_set(x_95, 1, x_94);
|
||||
x_11 = x_95;
|
||||
x_12 = x_91;
|
||||
goto block_15;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95;
|
||||
lean_dec(x_1);
|
||||
x_92 = lean_ctor_get(x_78, 1);
|
||||
lean_inc(x_92);
|
||||
lean_dec(x_78);
|
||||
x_93 = lean_ctor_get(x_79, 0);
|
||||
lean_inc(x_93);
|
||||
lean_dec(x_79);
|
||||
lean_inc(x_93);
|
||||
x_94 = l_Lean_Elab_Tactic_elabSimpArgs_isSimproc_x3f(x_93, x_6, x_7, x_8, x_9, x_92);
|
||||
x_95 = lean_ctor_get(x_94, 0);
|
||||
lean_inc(x_95);
|
||||
if (lean_obj_tag(x_95) == 0)
|
||||
{
|
||||
lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99;
|
||||
x_96 = lean_ctor_get(x_94, 1);
|
||||
x_96 = lean_ctor_get(x_83, 1);
|
||||
lean_inc(x_96);
|
||||
lean_dec(x_94);
|
||||
x_97 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_97, 0, x_93);
|
||||
lean_dec(x_83);
|
||||
x_97 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_97, 0, x_82);
|
||||
x_98 = lean_box(0);
|
||||
x_99 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_99, 0, x_97);
|
||||
|
|
@ -5249,38 +5248,69 @@ x_11 = x_99;
|
|||
x_12 = x_96;
|
||||
goto block_15;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104;
|
||||
lean_dec(x_93);
|
||||
x_100 = lean_ctor_get(x_94, 1);
|
||||
lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103;
|
||||
lean_dec(x_1);
|
||||
x_100 = lean_ctor_get(x_78, 1);
|
||||
lean_inc(x_100);
|
||||
lean_dec(x_94);
|
||||
x_101 = lean_ctor_get(x_95, 0);
|
||||
lean_dec(x_78);
|
||||
x_101 = lean_ctor_get(x_79, 0);
|
||||
lean_inc(x_101);
|
||||
lean_dec(x_95);
|
||||
x_102 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_102, 0, x_101);
|
||||
x_103 = lean_box(0);
|
||||
x_104 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_104, 0, x_102);
|
||||
lean_ctor_set(x_104, 1, x_103);
|
||||
x_11 = x_104;
|
||||
x_12 = x_100;
|
||||
lean_dec(x_79);
|
||||
lean_inc(x_101);
|
||||
x_102 = l_Lean_Elab_Tactic_elabSimpArgs_isSimproc_x3f(x_101, x_6, x_7, x_8, x_9, x_100);
|
||||
x_103 = lean_ctor_get(x_102, 0);
|
||||
lean_inc(x_103);
|
||||
if (lean_obj_tag(x_103) == 0)
|
||||
{
|
||||
lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107;
|
||||
x_104 = lean_ctor_get(x_102, 1);
|
||||
lean_inc(x_104);
|
||||
lean_dec(x_102);
|
||||
x_105 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_105, 0, x_101);
|
||||
x_106 = lean_box(0);
|
||||
x_107 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_107, 0, x_105);
|
||||
lean_ctor_set(x_107, 1, x_106);
|
||||
x_11 = x_107;
|
||||
x_12 = x_104;
|
||||
goto block_15;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112;
|
||||
lean_dec(x_101);
|
||||
x_108 = lean_ctor_get(x_102, 1);
|
||||
lean_inc(x_108);
|
||||
lean_dec(x_102);
|
||||
x_109 = lean_ctor_get(x_103, 0);
|
||||
lean_inc(x_109);
|
||||
lean_dec(x_103);
|
||||
x_110 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_110, 0, x_109);
|
||||
x_111 = lean_box(0);
|
||||
x_112 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_112, 0, x_110);
|
||||
lean_ctor_set(x_112, 1, x_111);
|
||||
x_11 = x_112;
|
||||
x_12 = x_108;
|
||||
goto block_15;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_105; lean_object* x_106;
|
||||
x_105 = lean_ctor_get(x_78, 0);
|
||||
lean_inc(x_105);
|
||||
x_106 = lean_ctor_get(x_78, 1);
|
||||
lean_inc(x_106);
|
||||
lean_object* x_113; lean_object* x_114;
|
||||
x_113 = lean_ctor_get(x_78, 0);
|
||||
lean_inc(x_113);
|
||||
x_114 = lean_ctor_get(x_78, 1);
|
||||
lean_inc(x_114);
|
||||
lean_dec(x_78);
|
||||
x_42 = x_105;
|
||||
x_43 = x_106;
|
||||
x_42 = x_113;
|
||||
x_43 = x_114;
|
||||
goto block_75;
|
||||
}
|
||||
block_75:
|
||||
|
|
@ -11308,7 +11338,7 @@ x_17 = l_Lean_Elab_Tactic_mkSimpContext(x_1, x_14, x_15, x_16, x_5, x_6, x_7, x_
|
|||
return x_17;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__1() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -11316,7 +11346,7 @@ x_1 = lean_mk_string_from_bytes("tactic", 6);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__2() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -11324,18 +11354,18 @@ x_1 = lean_mk_string_from_bytes("trace", 5);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__3() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__1;
|
||||
x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__1;
|
||||
x_2 = l_Lean_Elab_Tactic_tacticToDischarge___lambda__3___closed__1;
|
||||
x_3 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__2;
|
||||
x_3 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__2;
|
||||
x_4 = l_Lean_Name_mkStr3(x_1, x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__4() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -11343,13 +11373,13 @@ x_1 = lean_mk_string_from_bytes("When tracing is enabled, calls to `simp` or `ds
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__5() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__5() {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = 0;
|
||||
x_2 = l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_elabSimpArgs___spec__4___closed__3;
|
||||
x_3 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__4;
|
||||
x_3 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__4;
|
||||
x_4 = lean_box(x_1);
|
||||
x_5 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_5, 0, x_4);
|
||||
|
|
@ -11358,7 +11388,7 @@ lean_ctor_set(x_5, 2, x_3);
|
|||
return x_5;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__6() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -11366,27 +11396,27 @@ x_1 = lean_mk_string_from_bytes("Elab", 4);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__7() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__7() {
|
||||
_start:
|
||||
{
|
||||
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;
|
||||
x_1 = l_Lean_Elab_Tactic_evalUnsafe____x40_Lean_Elab_Tactic_Simp___hyg_7____closed__1;
|
||||
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__6;
|
||||
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__6;
|
||||
x_3 = l_Lean_Elab_Tactic_tacticToDischarge___closed__2;
|
||||
x_4 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__1;
|
||||
x_4 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__1;
|
||||
x_5 = l_Lean_Elab_Tactic_tacticToDischarge___lambda__3___closed__1;
|
||||
x_6 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__2;
|
||||
x_6 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__2;
|
||||
x_7 = l_Lean_Name_mkStr6(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230_(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__3;
|
||||
x_3 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__5;
|
||||
x_4 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__7;
|
||||
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__3;
|
||||
x_3 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__5;
|
||||
x_4 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__7;
|
||||
x_5 = l_Lean_Option_register___at_Lean_initFn____x40_Lean_PrettyPrinter_Delaborator_Options___hyg_6____spec__1(x_2, x_3, x_4, x_1);
|
||||
return x_5;
|
||||
}
|
||||
|
|
@ -15077,7 +15107,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = l_Lean_Elab_Tactic_evalUnsafe____x40_Lean_Elab_Tactic_Simp___hyg_7____closed__1;
|
||||
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__6;
|
||||
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__6;
|
||||
x_3 = l_Lean_Elab_Tactic_tacticToDischarge___closed__2;
|
||||
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalSimp___closed__2;
|
||||
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
|
||||
|
|
@ -15116,7 +15146,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange___c
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(375u);
|
||||
x_1 = lean_unsigned_to_nat(379u);
|
||||
x_2 = lean_unsigned_to_nat(42u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -15128,7 +15158,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange___c
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(380u);
|
||||
x_1 = lean_unsigned_to_nat(384u);
|
||||
x_2 = lean_unsigned_to_nat(31u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -15156,7 +15186,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange___c
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(375u);
|
||||
x_1 = lean_unsigned_to_nat(379u);
|
||||
x_2 = lean_unsigned_to_nat(46u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -15168,7 +15198,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimp_declRange___c
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(375u);
|
||||
x_1 = lean_unsigned_to_nat(379u);
|
||||
x_2 = lean_unsigned_to_nat(54u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -15583,7 +15613,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = l_Lean_Elab_Tactic_evalUnsafe____x40_Lean_Elab_Tactic_Simp___hyg_7____closed__1;
|
||||
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__6;
|
||||
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__6;
|
||||
x_3 = l_Lean_Elab_Tactic_tacticToDischarge___closed__2;
|
||||
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalSimpAll___closed__1;
|
||||
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
|
||||
|
|
@ -15614,7 +15644,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange_
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(382u);
|
||||
x_1 = lean_unsigned_to_nat(386u);
|
||||
x_2 = lean_unsigned_to_nat(45u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -15626,7 +15656,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange_
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(389u);
|
||||
x_1 = lean_unsigned_to_nat(393u);
|
||||
x_2 = lean_unsigned_to_nat(31u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -15654,7 +15684,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange_
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(382u);
|
||||
x_1 = lean_unsigned_to_nat(386u);
|
||||
x_2 = lean_unsigned_to_nat(49u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -15666,7 +15696,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange_
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(382u);
|
||||
x_1 = lean_unsigned_to_nat(386u);
|
||||
x_2 = lean_unsigned_to_nat(60u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -16335,7 +16365,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = l_Lean_Elab_Tactic_evalUnsafe____x40_Lean_Elab_Tactic_Simp___hyg_7____closed__1;
|
||||
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__6;
|
||||
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__6;
|
||||
x_3 = l_Lean_Elab_Tactic_tacticToDischarge___closed__2;
|
||||
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalDSimp___closed__3;
|
||||
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
|
||||
|
|
@ -16366,7 +16396,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalDSimp_declRange___
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(410u);
|
||||
x_1 = lean_unsigned_to_nat(414u);
|
||||
x_2 = lean_unsigned_to_nat(43u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -16378,7 +16408,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalDSimp_declRange___
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(412u);
|
||||
x_1 = lean_unsigned_to_nat(416u);
|
||||
x_2 = lean_unsigned_to_nat(46u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -16406,7 +16436,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalDSimp_declRange___
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(410u);
|
||||
x_1 = lean_unsigned_to_nat(414u);
|
||||
x_2 = lean_unsigned_to_nat(47u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -16418,7 +16448,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalDSimp_declRange___
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_unsigned_to_nat(410u);
|
||||
x_1 = lean_unsigned_to_nat(414u);
|
||||
x_2 = lean_unsigned_to_nat(56u);
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
|
|
@ -16701,21 +16731,21 @@ l_Lean_Elab_Tactic_mkSimpContext___closed__1 = _init_l_Lean_Elab_Tactic_mkSimpCo
|
|||
lean_mark_persistent(l_Lean_Elab_Tactic_mkSimpContext___closed__1);
|
||||
l_Lean_Elab_Tactic_mkSimpContext___closed__2 = _init_l_Lean_Elab_Tactic_mkSimpContext___closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_mkSimpContext___closed__2);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__1);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__2 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__2);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__3 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__3);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__4 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__4);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__5 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__5();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__5);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__6 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__6();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__6);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__7 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__7();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230____closed__7);
|
||||
if (builtin) {res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4230_(lean_io_mk_world());
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__1);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__2 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__2);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__3 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__3);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__4 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__4);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__5 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__5();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__5);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__6 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__6();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__6);
|
||||
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__7 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__7();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277____closed__7);
|
||||
if (builtin) {res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Simp___hyg_4277_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
l_Lean_Elab_Tactic_tactic_simp_trace = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_tactic_simp_trace);
|
||||
|
|
|
|||
798
stage0/stdlib/Lean/Elab/Tactic/Simproc.c
generated
798
stage0/stdlib/Lean/Elab/Tactic/Simproc.c
generated
File diff suppressed because it is too large
Load diff
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: Lean.Meta.Tactic.Simp.BuiltinSimprocs
|
||||
// Imports: Init Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
|
||||
// Imports: Init Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
|
|
@ -14,7 +14,11 @@
|
|||
extern "C" {
|
||||
#endif
|
||||
lean_object* initialize_Init(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Core(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs_UInt(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int(uint8_t builtin, lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
LEAN_EXPORT lean_object* initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs(uint8_t builtin, lean_object* w) {
|
||||
lean_object * res;
|
||||
|
|
@ -23,9 +27,21 @@ _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_BuiltinSimprocs_Core(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Nat(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Fin(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs_UInt(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Lean_Meta_Tactic_Simp_BuiltinSimprocs_Int(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
1442
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.c
generated
Normal file
1442
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.c
generated
Normal file
File diff suppressed because it is too large
Load diff
10202
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.c
generated
Normal file
10202
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.c
generated
Normal file
File diff suppressed because it is too large
Load diff
10840
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.c
generated
Normal file
10840
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.c
generated
Normal file
File diff suppressed because it is too large
Load diff
1829
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.c
generated
1829
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.c
generated
File diff suppressed because it is too large
Load diff
52757
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.c
generated
Normal file
52757
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.c
generated
Normal file
File diff suppressed because one or more lines are too long
3919
stage0/stdlib/Lean/Meta/Tactic/Simp/Simproc.c
generated
3919
stage0/stdlib/Lean/Meta/Tactic/Simp/Simproc.c
generated
File diff suppressed because it is too large
Load diff
Loading…
Add table
Reference in a new issue