chore: update stage0
This commit is contained in:
Lean stage0 autoupdater
parent
0de925eafc
commit
cd24e9dad4
11 changed files with 5987 additions and 6202 deletions
6315
stage0/stdlib/Lake/Build/Common.c
generated
6315
stage0/stdlib/Lake/Build/Common.c
generated
File diff suppressed because it is too large
Load diff
125
stage0/stdlib/Lake/Build/Job.c
generated
125
stage0/stdlib/Lake/Build/Job.c
generated
|
|
@ -25,6 +25,7 @@ LEAN_EXPORT lean_object* l_IO_FS_withIsolatedStreams___at_Lake_Job_async___spec_
|
|||
LEAN_EXPORT lean_object* l_Lake_Job_renew___rarg___lambda__1(lean_object*);
|
||||
static lean_object* l___private_Lake_Build_Job_0__Lake_reprJobAction____x40_Lake_Build_Job___hyg_18____closed__5;
|
||||
LEAN_EXPORT lean_object* l_Lake_BuildJob_collectList(lean_object*);
|
||||
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
|
||||
static lean_object* l_Lake_instMonadLogJobM___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lake_Job_bindSync(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lake_BuildJob_pure___rarg(lean_object*);
|
||||
|
|
@ -69,7 +70,6 @@ uint8_t lean_usize_dec_eq(size_t, size_t);
|
|||
static lean_object* l_Lake_Job_instFunctor___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lake_BuildJob_collectList___rarg(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lake_BuildJob_bindAsync(lean_object*, lean_object*);
|
||||
static lean_object* l_Lake_BuildJob_collectArray___rarg___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lake_Job_setCaption_x3f___rarg(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Lake_BuildJob_mixList___spec__3___rarg(lean_object*, size_t, size_t, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lake_BuildJob_mk___rarg___boxed(lean_object*);
|
||||
|
|
@ -81,7 +81,6 @@ static lean_object* l_Lake_instCoeOutJobOpaqueJob___closed__1;
|
|||
LEAN_EXPORT lean_object* l_Lake_JobAction_noConfusion(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Lake_BuildJob_collectList___spec__2___at_Lake_BuildJob_collectList___spec__5___rarg___lambda__1(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_IO_withStdout___at_Lake_Job_async___spec__2(lean_object*);
|
||||
static lean_object* l_Lake_BuildJob_collectArray___rarg___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lake_instCoeOutJobOpaqueJob(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lake_Job_renew___rarg(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lake_instOrdJobAction;
|
||||
|
|
@ -172,7 +171,6 @@ LEAN_EXPORT lean_object* l_Lake_Job_ofTask(lean_object*);
|
|||
static lean_object* l_Lake_BuildJob_instFunctor___closed__2;
|
||||
static lean_object* l_Lake_BuildJob_nil___closed__2;
|
||||
lean_object* l_Function_const___rarg___boxed(lean_object*, lean_object*);
|
||||
static lean_object* l_Lake_BuildJob_collectArray___rarg___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Lake_BuildJob_mixList___spec__2___rarg___lambda__2(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_IO_FS_withIsolatedStreams___at_Lake_BuildJob_bindSync___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_st_ref_get(lean_object*, lean_object*);
|
||||
|
|
@ -345,7 +343,6 @@ LEAN_EXPORT lean_object* l_Lake_instMonadLiftLakeMBuildTOfPure(lean_object*);
|
|||
static lean_object* l_Lake_JobAction_verb___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lake_Job_renew(lean_object*);
|
||||
size_t lean_usize_sub(size_t, size_t);
|
||||
static lean_object* l_Lake_BuildJob_collectArray___rarg___closed__4;
|
||||
lean_object* lean_array_mk(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lake_Job_zipWith___rarg___lambda__2(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
|
||||
LEAN_EXPORT uint8_t l_Lake_JobAction_ofNat(lean_object*);
|
||||
|
|
@ -25096,88 +25093,52 @@ x_2 = lean_alloc_closure((void*)(l_Array_foldlMUnsafe_fold___at_Lake_BuildJob_co
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lake_BuildJob_collectArray___rarg___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lake_instInhabitedJobState___closed__1;
|
||||
x_2 = l_Lake_BuildTrace_nil;
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lake_BuildJob_collectArray___rarg___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lake_BuildJob_collectArray___rarg___closed__1;
|
||||
x_2 = l_Lake_instInhabitedJobState___closed__2;
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lake_BuildJob_collectArray___rarg___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lake_BuildJob_collectArray___rarg___closed__2;
|
||||
x_2 = lean_task_pure(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lake_BuildJob_collectArray___rarg___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
|
||||
x_1 = l_Lake_BuildJob_collectArray___rarg___closed__3;
|
||||
x_2 = l_Lake_Job_instPure___rarg___closed__1;
|
||||
x_3 = 0;
|
||||
x_4 = lean_alloc_ctor(0, 2, 1);
|
||||
lean_ctor_set(x_4, 0, x_1);
|
||||
lean_ctor_set(x_4, 1, x_2);
|
||||
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lake_BuildJob_collectArray___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; uint8_t x_4;
|
||||
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; uint8_t x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13;
|
||||
x_2 = lean_array_get_size(x_1);
|
||||
x_3 = lean_unsigned_to_nat(0u);
|
||||
x_4 = lean_nat_dec_lt(x_3, x_2);
|
||||
if (x_4 == 0)
|
||||
x_3 = lean_mk_empty_array_with_capacity(x_2);
|
||||
x_4 = l_Lake_BuildTrace_nil;
|
||||
x_5 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_5, 0, x_3);
|
||||
lean_ctor_set(x_5, 1, x_4);
|
||||
x_6 = l_Lake_instInhabitedJobState___closed__2;
|
||||
x_7 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_7, 0, x_5);
|
||||
lean_ctor_set(x_7, 1, x_6);
|
||||
x_8 = lean_task_pure(x_7);
|
||||
x_9 = l_Lake_Job_instPure___rarg___closed__1;
|
||||
x_10 = 0;
|
||||
x_11 = lean_alloc_ctor(0, 2, 1);
|
||||
lean_ctor_set(x_11, 0, x_8);
|
||||
lean_ctor_set(x_11, 1, x_9);
|
||||
lean_ctor_set_uint8(x_11, sizeof(void*)*2, x_10);
|
||||
x_12 = lean_unsigned_to_nat(0u);
|
||||
x_13 = lean_nat_dec_lt(x_12, x_2);
|
||||
if (x_13 == 0)
|
||||
{
|
||||
lean_object* x_5;
|
||||
lean_dec(x_2);
|
||||
x_5 = l_Lake_BuildJob_collectArray___rarg___closed__4;
|
||||
return x_5;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_6;
|
||||
x_6 = lean_nat_dec_le(x_2, x_2);
|
||||
if (x_6 == 0)
|
||||
{
|
||||
lean_object* x_7;
|
||||
lean_dec(x_2);
|
||||
x_7 = l_Lake_BuildJob_collectArray___rarg___closed__4;
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
size_t x_8; size_t x_9; lean_object* x_10; lean_object* x_11;
|
||||
x_8 = 0;
|
||||
x_9 = lean_usize_of_nat(x_2);
|
||||
lean_dec(x_2);
|
||||
x_10 = l_Lake_BuildJob_collectArray___rarg___closed__4;
|
||||
x_11 = l_Array_foldlMUnsafe_fold___at_Lake_BuildJob_collectArray___spec__1___at_Lake_BuildJob_collectArray___spec__2___rarg(x_1, x_8, x_9, x_10);
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_14;
|
||||
x_14 = lean_nat_dec_le(x_2, x_2);
|
||||
if (x_14 == 0)
|
||||
{
|
||||
lean_dec(x_2);
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
size_t x_15; size_t x_16; lean_object* x_17;
|
||||
x_15 = 0;
|
||||
x_16 = lean_usize_of_nat(x_2);
|
||||
lean_dec(x_2);
|
||||
x_17 = l_Array_foldlMUnsafe_fold___at_Lake_BuildJob_collectArray___spec__1___at_Lake_BuildJob_collectArray___spec__2___rarg(x_1, x_15, x_16, x_11);
|
||||
return x_17;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -25448,14 +25409,6 @@ l_Lake_BuildJob_collectList___rarg___closed__4 = _init_l_Lake_BuildJob_collectLi
|
|||
lean_mark_persistent(l_Lake_BuildJob_collectList___rarg___closed__4);
|
||||
l_Array_foldlMUnsafe_fold___at_Lake_BuildJob_collectArray___spec__1___at_Lake_BuildJob_collectArray___spec__2___rarg___closed__1 = _init_l_Array_foldlMUnsafe_fold___at_Lake_BuildJob_collectArray___spec__1___at_Lake_BuildJob_collectArray___spec__2___rarg___closed__1();
|
||||
lean_mark_persistent(l_Array_foldlMUnsafe_fold___at_Lake_BuildJob_collectArray___spec__1___at_Lake_BuildJob_collectArray___spec__2___rarg___closed__1);
|
||||
l_Lake_BuildJob_collectArray___rarg___closed__1 = _init_l_Lake_BuildJob_collectArray___rarg___closed__1();
|
||||
lean_mark_persistent(l_Lake_BuildJob_collectArray___rarg___closed__1);
|
||||
l_Lake_BuildJob_collectArray___rarg___closed__2 = _init_l_Lake_BuildJob_collectArray___rarg___closed__2();
|
||||
lean_mark_persistent(l_Lake_BuildJob_collectArray___rarg___closed__2);
|
||||
l_Lake_BuildJob_collectArray___rarg___closed__3 = _init_l_Lake_BuildJob_collectArray___rarg___closed__3();
|
||||
lean_mark_persistent(l_Lake_BuildJob_collectArray___rarg___closed__3);
|
||||
l_Lake_BuildJob_collectArray___rarg___closed__4 = _init_l_Lake_BuildJob_collectArray___rarg___closed__4();
|
||||
lean_mark_persistent(l_Lake_BuildJob_collectArray___rarg___closed__4);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
2760
stage0/stdlib/Lake/Build/Module.c
generated
2760
stage0/stdlib/Lake/Build/Module.c
generated
File diff suppressed because it is too large
Load diff
816
stage0/stdlib/Lake/Build/Trace.c
generated
816
stage0/stdlib/Lake/Build/Trace.c
generated
File diff suppressed because it is too large
Load diff
6
stage0/stdlib/Lean/Compiler/CSimpAttr.c
generated
6
stage0/stdlib/Lean/Compiler/CSimpAttr.c
generated
|
|
@ -44,7 +44,6 @@ static lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr_
|
|||
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at_Lean_Compiler_CSimp_replaceConstants___spec__3___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_fget(lean_object*, lean_object*);
|
||||
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6488____spec__4(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Compiler_CSimp_instInhabitedState;
|
||||
static lean_object* l_Lean_Compiler_CSimp_instInhabitedState___closed__5;
|
||||
LEAN_EXPORT lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_137_(lean_object*);
|
||||
|
|
@ -106,6 +105,7 @@ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at_Lean_Compiler_C
|
|||
lean_object* lean_usize_to_nat(size_t);
|
||||
LEAN_EXPORT uint8_t l_Lean_Compiler_hasCSimpAttribute(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_MessageData_ofConstName(lean_object*, uint8_t);
|
||||
lean_object* l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6513____spec__4(lean_object*);
|
||||
static lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_471____closed__18;
|
||||
static lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_471____closed__17;
|
||||
static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Compiler_CSimp_add___spec__2___closed__1;
|
||||
|
|
@ -330,7 +330,7 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
|||
x_3 = lean_ctor_get(x_1, 0);
|
||||
x_4 = lean_ctor_get(x_1, 1);
|
||||
x_5 = l_Lean_SMap_switch___at_Lean_Compiler_CSimp_State_switch___spec__1(x_3);
|
||||
x_6 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6488____spec__4(x_4);
|
||||
x_6 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6513____spec__4(x_4);
|
||||
lean_ctor_set(x_1, 1, x_6);
|
||||
lean_ctor_set(x_1, 0, x_5);
|
||||
return x_1;
|
||||
|
|
@ -344,7 +344,7 @@ lean_inc(x_8);
|
|||
lean_inc(x_7);
|
||||
lean_dec(x_1);
|
||||
x_9 = l_Lean_SMap_switch___at_Lean_Compiler_CSimp_State_switch___spec__1(x_7);
|
||||
x_10 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6488____spec__4(x_8);
|
||||
x_10 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6513____spec__4(x_8);
|
||||
x_11 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_11, 0, x_9);
|
||||
lean_ctor_set(x_11, 1, x_10);
|
||||
|
|
|
|||
2
stage0/stdlib/Lean/Compiler/LCNF/JoinPoints.c
generated
2
stage0/stdlib/Lean/Compiler/LCNF/JoinPoints.c
generated
|
|
@ -16008,7 +16008,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;
|
||||
x_1 = l_Lean_Compiler_LCNF_JoinPointCommonArgs_isInJpScope___closed__1;
|
||||
x_2 = l_Lean_Compiler_LCNF_JoinPointCommonArgs_isInJpScope___closed__2;
|
||||
x_3 = lean_unsigned_to_nat(384u);
|
||||
x_3 = lean_unsigned_to_nat(389u);
|
||||
x_4 = lean_unsigned_to_nat(14u);
|
||||
x_5 = l_Lean_Compiler_LCNF_JoinPointCommonArgs_isInJpScope___closed__3;
|
||||
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
|
||||
|
|
|
|||
72
stage0/stdlib/Lean/Data/RBMap.c
generated
72
stage0/stdlib/Lean/Data/RBMap.c
generated
|
|
@ -98,6 +98,7 @@ static lean_object* l_List_repr___at_Lean_RBMap_instRepr___spec__1___rarg___clos
|
|||
LEAN_EXPORT lean_object* l_Lean_RBMap_isSingleton___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_instRepr(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBNode_size___rarg___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_toArray___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_lowerBound___rarg(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_instForInProd___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_isSingleton(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -197,6 +198,7 @@ LEAN_EXPORT lean_object* l_Lean_instEmptyCollectionRBMap(lean_object*, lean_obje
|
|||
LEAN_EXPORT lean_object* l_Lean_RBMap_insert(lean_object*, lean_object*);
|
||||
LEAN_EXPORT uint8_t l_Lean_RBMap_any___rarg(lean_object*, lean_object*);
|
||||
LEAN_EXPORT uint8_t l_Lean_RBNode_any___rarg(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_toArray___rarg(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_all___rarg___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBNode_mapM___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBNode_forM___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -204,6 +206,7 @@ LEAN_EXPORT lean_object* l_Lean_RBNode_min(lean_object*, lean_object*);
|
|||
static lean_object* l_Prod_repr___at_Lean_RBMap_instRepr___spec__3___rarg___closed__8;
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_ofList___rarg(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_RBMap_find_x21___rarg___closed__2;
|
||||
static lean_object* l_Lean_RBMap_toArray___rarg___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_RBColor_noConfusion___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_List_repr___at_Lean_RBMap_instRepr___spec__1___rarg___closed__1;
|
||||
static lean_object* l_Lean_RBMap_instRepr___rarg___closed__1;
|
||||
|
|
@ -213,6 +216,8 @@ LEAN_EXPORT lean_object* l_Lean_RBNode_depth(lean_object*, lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Lean_RBNode_max___rarg___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_forIn___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBNode_fold(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_toArray___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_RBMap_toArray___rarg___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_RBNode_isRed___rarg___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_List_repr___at_Lean_RBMap_instRepr___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Format_joinSep___at_Lean_RBMap_instRepr___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -278,6 +283,7 @@ LEAN_EXPORT lean_object* l_Lean_RBNode_toArray___rarg___boxed(lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Lean_RBNode_depth___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_List_reverse___rarg(lean_object*);
|
||||
static lean_object* l_Lean_RBMap_min_x21___rarg___closed__3;
|
||||
lean_object* lean_array_mk(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBNode_lowerBound(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_min___rarg(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_instInhabitedRBMap(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -313,6 +319,7 @@ LEAN_EXPORT lean_object* l_Lean_RBMap_isSingleton___rarg___boxed(lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Lean_RBNode_forIn_visit___at_Lean_RBMap_instForInProd___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBNode_map(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_max_x21___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_toArray(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Prod_repr___at_Lean_RBMap_instRepr___spec__3___rarg___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_RBNode_min___rarg(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_mergeBy(lean_object*, lean_object*);
|
||||
|
|
@ -20986,6 +20993,61 @@ lean_dec(x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_toArray___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5;
|
||||
x_4 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_4, 0, x_2);
|
||||
lean_ctor_set(x_4, 1, x_3);
|
||||
x_5 = lean_array_push(x_1, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_RBMap_toArray___rarg___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = lean_array_mk(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_RBMap_toArray___rarg___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_RBMap_toArray___rarg___lambda__1), 3, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_toArray___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_2 = l_Lean_RBMap_toArray___rarg___closed__2;
|
||||
x_3 = l_Lean_RBMap_toArray___rarg___closed__1;
|
||||
x_4 = l_Lean_RBNode_fold___rarg(x_2, x_3, x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_toArray(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_Lean_RBMap_toArray___rarg), 1, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_toArray___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Lean_RBMap_toArray(x_1, x_2, x_3);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_RBMap_min___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -22300,7 +22362,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;
|
||||
x_1 = l_Lean_RBMap_min_x21___rarg___closed__1;
|
||||
x_2 = l_Lean_RBMap_min_x21___rarg___closed__2;
|
||||
x_3 = lean_unsigned_to_nat(373u);
|
||||
x_3 = lean_unsigned_to_nat(378u);
|
||||
x_4 = lean_unsigned_to_nat(14u);
|
||||
x_5 = l_Lean_RBMap_min_x21___rarg___closed__3;
|
||||
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
|
||||
|
|
@ -22407,7 +22469,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;
|
||||
x_1 = l_Lean_RBMap_min_x21___rarg___closed__1;
|
||||
x_2 = l_Lean_RBMap_max_x21___rarg___closed__1;
|
||||
x_3 = lean_unsigned_to_nat(378u);
|
||||
x_3 = lean_unsigned_to_nat(383u);
|
||||
x_4 = lean_unsigned_to_nat(14u);
|
||||
x_5 = l_Lean_RBMap_min_x21___rarg___closed__3;
|
||||
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
|
||||
|
|
@ -22503,7 +22565,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;
|
||||
x_1 = l_Lean_RBMap_min_x21___rarg___closed__1;
|
||||
x_2 = l_Lean_RBMap_find_x21___rarg___closed__1;
|
||||
x_3 = lean_unsigned_to_nat(384u);
|
||||
x_3 = lean_unsigned_to_nat(389u);
|
||||
x_4 = lean_unsigned_to_nat(14u);
|
||||
x_5 = l_Lean_RBMap_find_x21___rarg___closed__2;
|
||||
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
|
||||
|
|
@ -22778,6 +22840,10 @@ l_Lean_RBNode_toArray___rarg___closed__1 = _init_l_Lean_RBNode_toArray___rarg___
|
|||
lean_mark_persistent(l_Lean_RBNode_toArray___rarg___closed__1);
|
||||
l_Lean_RBMap_toList___rarg___closed__1 = _init_l_Lean_RBMap_toList___rarg___closed__1();
|
||||
lean_mark_persistent(l_Lean_RBMap_toList___rarg___closed__1);
|
||||
l_Lean_RBMap_toArray___rarg___closed__1 = _init_l_Lean_RBMap_toArray___rarg___closed__1();
|
||||
lean_mark_persistent(l_Lean_RBMap_toArray___rarg___closed__1);
|
||||
l_Lean_RBMap_toArray___rarg___closed__2 = _init_l_Lean_RBMap_toArray___rarg___closed__2();
|
||||
lean_mark_persistent(l_Lean_RBMap_toArray___rarg___closed__2);
|
||||
l_Prod_repr___at_Lean_RBMap_instRepr___spec__3___rarg___closed__1 = _init_l_Prod_repr___at_Lean_RBMap_instRepr___spec__3___rarg___closed__1();
|
||||
lean_mark_persistent(l_Prod_repr___at_Lean_RBMap_instRepr___spec__3___rarg___closed__1);
|
||||
l_Prod_repr___at_Lean_RBMap_instRepr___spec__3___rarg___closed__2 = _init_l_Prod_repr___at_Lean_RBMap_instRepr___spec__3___rarg___closed__2();
|
||||
|
|
|
|||
374
stage0/stdlib/Lean/Elab/Tactic/Omega/Frontend.c
generated
374
stage0/stdlib/Lean/Elab/Tactic/Omega/Frontend.c
generated
|
|
@ -27,6 +27,7 @@ lean_object* l_Lean_Expr_const___override(lean_object*, lean_object*);
|
|||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__6___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__22(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_mkCoordinateEvalAtomsEq___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___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_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_mkEvalRflProof___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*);
|
||||
|
|
@ -39,7 +40,6 @@ static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__6___clo
|
|||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__35___closed__10;
|
||||
LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_AssocList_foldlM___at_Lean_Elab_Tactic_Omega_asLinearCombo___spec__6(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__10___closed__13;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___closed__1;
|
||||
lean_object* l_Lean_isTracingEnabledFor___at_Lean_Elab_Tactic_Omega_lookup___spec__2___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_Omega_MetaProblem_addIntEquality___closed__4;
|
||||
lean_object* l_Lean_mkNatLit(lean_object*);
|
||||
|
|
@ -141,7 +141,6 @@ static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__22___
|
|||
lean_object* l_Lean_MessageData_joinSep(lean_object*, lean_object*);
|
||||
size_t lean_uint64_to_usize(uint64_t);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___closed__4;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_formatErrorMessage_varNameOf(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__16(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_Omega_omegaTactic___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -153,11 +152,13 @@ lean_object* l_Lean_Expr_lit___override(lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addIntInequality___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___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___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__7;
|
||||
lean_object* l_Lean_Elab_Tactic_Omega_withoutModifyingState___rarg(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_MessageData_ofList(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_formatErrorMessage_inScope(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__33___closed__2;
|
||||
lean_object* lean_array_push(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__1;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleNatCast___closed__28;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__20(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -193,11 +194,10 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_omegaImpl___boxed(lean_object*
|
|||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__33___closed__1;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_formatErrorMessage_varNames___closed__1;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_mkEvalRflProof___closed__8;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__3;
|
||||
static lean_object* l_panic___at_Lean_Elab_Tactic_Omega_asLinearComboImpl_rewrite___spec__1___closed__5;
|
||||
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__8;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__23___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__32___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*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___closed__3;
|
||||
lean_object* lean_array_fget(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Expr_instBEq;
|
||||
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -242,7 +242,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_formatErrorMessage_inScope___l
|
|||
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_Omega_elabOmegaConfig___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_formatErrorMessage_prettyConstraint(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_mkCoordinateEvalAtomsEq___closed__1;
|
||||
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__15___closed__2;
|
||||
lean_object* l_Lean_Name_mkStr5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -288,7 +287,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__
|
|||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__22___closed__7;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_omegaImpl___lambda__4___closed__4;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__8___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___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_Lean_Elab_Tactic_Omega_evalUnsafe____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_6____closed__2;
|
||||
lean_object* lean_string_push(lean_object*, uint32_t);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__5___closed__2;
|
||||
|
|
@ -375,6 +373,7 @@ static lean_object* l_Lean_Elab_Tactic_Omega_elabOmegaConfig___lambda__4___close
|
|||
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_Omega_omegaTactic___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*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_formatErrorMessage_inScope___closed__1;
|
||||
uint8_t lean_expr_eqv(lean_object*, lean_object*);
|
||||
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__6;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_evalUnsafe____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_6____closed__1;
|
||||
lean_object* l_Array_zip___rarg(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__14___closed__1;
|
||||
|
|
@ -468,7 +467,6 @@ static lean_object* l_Lean_Elab_Tactic_Omega_formatErrorMessage_prettyConstraint
|
|||
lean_object* l_Lean_Elab_Tactic_withMainContext___rarg(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_Omega_asLinearComboImpl_handleNatCast___closed__46;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__19___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___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_List_mapTR_loop___at_Lean_Elab_Tactic_Omega_formatErrorMessage_prettyCoeffs___spec__2___closed__3;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__10___closed__25;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__24___closed__2;
|
||||
|
|
@ -550,7 +548,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__2_
|
|||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__19___closed__3;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_mkEvalRflProof___closed__6;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_trivial;
|
||||
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_MVarId_elabFalseOrByContra___spec__1___rarg(lean_object*);
|
||||
extern lean_object* l_String_instInhabited;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_omegaImpl___lambda__6___closed__2;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__9___closed__2;
|
||||
|
|
@ -563,13 +560,13 @@ static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___closed__1;
|
|||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleNatCast___closed__41;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_mkCoordinateEvalAtomsEq___closed__2;
|
||||
uint8_t l_Lean_Expr_isArrow(lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__5;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__1___closed__7;
|
||||
lean_object* l_Lean_Elab_Tactic_Omega_mkEqReflWithExpectedType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_elabOmegaConfig(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_Omega_MetaProblem_addFact___lambda__15___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__25(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_omegaTactic___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkOptionalNode(lean_object*);
|
||||
lean_object* l_Lean_Elab_Tactic_Omega_Problem_addEquality(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl_rewrite___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_omegaImpl___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*);
|
||||
|
|
@ -577,7 +574,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__2(
|
|||
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__1(lean_object*, lean_object*, lean_object*, 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___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Syntax_matchesNull(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__2___closed__1;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_mkEvalRflProof___closed__9;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__9___closed__2;
|
||||
|
|
@ -606,6 +602,7 @@ static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__21___
|
|||
LEAN_EXPORT lean_object* l_Lean_instantiateMVars___at_Lean_Elab_Tactic_Omega_MetaProblem_addFact___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__22___closed__10;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_omegaImpl___lambda__3___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*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967_(lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__6___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_MVarId_withContext___at_Lean_Elab_Tactic_Omega_splitDisjunction___spec__2(lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_trivial___closed__1;
|
||||
|
|
@ -618,6 +615,7 @@ static lean_object* l_Lean_Elab_Tactic_Omega_cases_u2082___closed__1;
|
|||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addIntEquality___closed__2;
|
||||
lean_object* l_Lean_Elab_Tactic_Omega_atomsList___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_cases_u2082___closed__2;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__3;
|
||||
uint8_t l_List_decidableBAll___rarg(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__10___closed__39;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__10___closed__19;
|
||||
|
|
@ -631,14 +629,12 @@ LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_Omeg
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__9___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*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleNatCast___closed__60;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__27___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*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_Omega_cases_u2082___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleFinVal___closed__6;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__1___closed__8;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__10___closed__12;
|
||||
lean_object* lean_mk_thunk(lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___closed__2;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl_rewrite___closed__2;
|
||||
LEAN_EXPORT lean_object* l_List_elem___at_Lean_Elab_Tactic_Omega_MetaProblem_addFact___spec__2___boxed(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleNatCast___closed__40;
|
||||
|
|
@ -743,6 +739,7 @@ static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__10___cl
|
|||
lean_object* l_Lean_Elab_Tactic_Omega_Problem_addInequality(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_mkEvalRflProof___closed__23;
|
||||
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__2;
|
||||
LEAN_EXPORT lean_object* l_List_filterTR_loop___at_Lean_Elab_Tactic_Omega_formatErrorMessage_prettyAtoms___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_nat_mod(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -764,7 +761,6 @@ static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__35___
|
|||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__35___closed__11;
|
||||
lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__10(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_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__5;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__4___closed__1;
|
||||
lean_object* l_Lean_Meta_mkEqRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__21___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*);
|
||||
|
|
@ -797,7 +793,6 @@ lean_object* l_Int_toNat(lean_object*);
|
|||
static lean_object* l_Lean_Elab_Tactic_Omega_formatErrorMessage_prettyAtoms___closed__1;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_succ_x3f___closed__3;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl___lambda__10___closed__23;
|
||||
uint8_t l_Lean_Syntax_isNone(lean_object*);
|
||||
lean_object* lean_panic_fn(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_Elab_Tactic_Omega_formatErrorMessage_prettyConstraints___spec__1___lambda__1___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -873,11 +868,10 @@ lean_object* l_Lean_instantiateMVarsCore(lean_object*, lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_evalUnsafe____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_6_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_MVarId_assign___at_Lean_Elab_Tactic_Omega_omegaImpl___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_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__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*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___lambda__1___closed__1;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_mkEvalRflProof___closed__12;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleFinVal___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___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*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__4;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__4;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__3___closed__2;
|
||||
size_t lean_usize_add(size_t, size_t);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_formatErrorMessage_prettyConstraints(lean_object*, lean_object*);
|
||||
|
|
@ -921,7 +915,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__
|
|||
static lean_object* l_Lean_Elab_Tactic_Omega_formatErrorMessage_prettyConstraint___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_splitDisjunction___lambda__7(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_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__35(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__1;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__20___closed__3;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleNatCast___closed__48;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_pushNot___lambda__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -996,7 +989,6 @@ LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_AssocList_get_x3f___at_Lean_Ela
|
|||
lean_object* lean_nat_add(lean_object*, lean_object*);
|
||||
static lean_object* l_panic___at_Lean_Elab_Tactic_Omega_asLinearComboImpl_rewrite___spec__1___closed__8;
|
||||
static lean_object* l_Lean_Elab_Tactic_Omega_MetaProblem_addFact___lambda__31___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061_(lean_object*);
|
||||
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_Omega_Problem_instToString___spec__3(lean_object*, size_t, size_t, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_Omega_MetaProblem_addIntInequality___spec__2(lean_object*, lean_object*, size_t, size_t, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleFinVal___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*);
|
||||
|
|
@ -37304,29 +37296,19 @@ x_11 = l_Lean_Elab_Tactic_Omega_omegaTactic(x_10, x_1, x_2, x_3, x_4, x_5, x_6,
|
|||
return x_11;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_evalOmega___lambda__1___closed__1() {
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_evalOmega(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) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_mkOptionalNode(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___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) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_2) == 0)
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13;
|
||||
x_12 = l_Lean_Elab_Tactic_Omega_evalOmega___lambda__1___closed__1;
|
||||
lean_inc(x_10);
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_11 = lean_unsigned_to_nat(1u);
|
||||
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
|
||||
lean_inc(x_9);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
x_13 = l_Lean_Elab_Tactic_Omega_elabOmegaConfig(x_12, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
|
||||
lean_inc(x_4);
|
||||
x_13 = l_Lean_Elab_Tactic_Omega_elabOmegaConfig(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
|
||||
if (lean_obj_tag(x_13) == 0)
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16;
|
||||
|
|
@ -37335,13 +37317,12 @@ lean_inc(x_14);
|
|||
x_15 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_15);
|
||||
lean_dec(x_13);
|
||||
x_16 = l_Lean_Elab_Tactic_Omega_omegaTactic(x_14, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_15);
|
||||
x_16 = l_Lean_Elab_Tactic_Omega_omegaTactic(x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_15);
|
||||
return x_16;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_17;
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
|
|
@ -37349,6 +37330,7 @@ lean_dec(x_6);
|
|||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
x_17 = !lean_is_exclusive(x_13);
|
||||
if (x_17 == 0)
|
||||
{
|
||||
|
|
@ -37369,129 +37351,17 @@ return x_20;
|
|||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___boxed(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) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_21;
|
||||
x_21 = !lean_is_exclusive(x_2);
|
||||
if (x_21 == 0)
|
||||
{
|
||||
lean_object* x_22; lean_object* x_23;
|
||||
x_22 = l_Lean_mkOptionalNode(x_2);
|
||||
lean_dec(x_2);
|
||||
lean_inc(x_10);
|
||||
lean_inc(x_9);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
x_23 = l_Lean_Elab_Tactic_Omega_elabOmegaConfig(x_22, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
|
||||
if (lean_obj_tag(x_23) == 0)
|
||||
{
|
||||
lean_object* x_24; lean_object* x_25; lean_object* x_26;
|
||||
x_24 = lean_ctor_get(x_23, 0);
|
||||
lean_inc(x_24);
|
||||
x_25 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_25);
|
||||
lean_dec(x_23);
|
||||
x_26 = l_Lean_Elab_Tactic_Omega_omegaTactic(x_24, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_25);
|
||||
return x_26;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_27;
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_27 = !lean_is_exclusive(x_23);
|
||||
if (x_27 == 0)
|
||||
{
|
||||
return x_23;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_28; lean_object* x_29; lean_object* x_30;
|
||||
x_28 = lean_ctor_get(x_23, 0);
|
||||
x_29 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_29);
|
||||
lean_inc(x_28);
|
||||
lean_dec(x_23);
|
||||
x_30 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_30, 0, x_28);
|
||||
lean_ctor_set(x_30, 1, x_29);
|
||||
return x_30;
|
||||
lean_object* x_11;
|
||||
x_11 = l_Lean_Elab_Tactic_Omega_evalOmega(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
|
||||
lean_dec(x_1);
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
|
||||
x_31 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_31);
|
||||
lean_dec(x_2);
|
||||
x_32 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_32, 0, x_31);
|
||||
x_33 = l_Lean_mkOptionalNode(x_32);
|
||||
lean_dec(x_32);
|
||||
lean_inc(x_10);
|
||||
lean_inc(x_9);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
x_34 = l_Lean_Elab_Tactic_Omega_elabOmegaConfig(x_33, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
|
||||
if (lean_obj_tag(x_34) == 0)
|
||||
{
|
||||
lean_object* x_35; lean_object* x_36; lean_object* x_37;
|
||||
x_35 = lean_ctor_get(x_34, 0);
|
||||
lean_inc(x_35);
|
||||
x_36 = lean_ctor_get(x_34, 1);
|
||||
lean_inc(x_36);
|
||||
lean_dec(x_34);
|
||||
x_37 = l_Lean_Elab_Tactic_Omega_omegaTactic(x_35, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_36);
|
||||
return x_37;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_38 = lean_ctor_get(x_34, 0);
|
||||
lean_inc(x_38);
|
||||
x_39 = lean_ctor_get(x_34, 1);
|
||||
lean_inc(x_39);
|
||||
if (lean_is_exclusive(x_34)) {
|
||||
lean_ctor_release(x_34, 0);
|
||||
lean_ctor_release(x_34, 1);
|
||||
x_40 = x_34;
|
||||
} else {
|
||||
lean_dec_ref(x_34);
|
||||
x_40 = lean_box(0);
|
||||
}
|
||||
if (lean_is_scalar(x_40)) {
|
||||
x_41 = lean_alloc_ctor(1, 2, 0);
|
||||
} else {
|
||||
x_41 = x_40;
|
||||
}
|
||||
lean_ctor_set(x_41, 0, x_38);
|
||||
lean_ctor_set(x_41, 1, x_39);
|
||||
return x_41;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_evalOmega___closed__1() {
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -37499,7 +37369,7 @@ x_1 = lean_mk_string_unchecked("Parser", 6, 6);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_evalOmega___closed__2() {
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -37507,111 +37377,19 @@ x_1 = lean_mk_string_unchecked("Tactic", 6, 6);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_evalOmega___closed__3() {
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__3() {
|
||||
_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_Omega_evalUnsafe____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_6____closed__1;
|
||||
x_2 = l_Lean_Elab_Tactic_Omega_evalOmega___closed__1;
|
||||
x_3 = l_Lean_Elab_Tactic_Omega_evalOmega___closed__2;
|
||||
x_2 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__1;
|
||||
x_3 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__2;
|
||||
x_4 = l_Lean_Elab_Tactic_Omega_asLinearComboImpl_rewrite___closed__1;
|
||||
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_evalOmega___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_Omega_evalOmega___lambda__1___boxed), 11, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_evalOmega(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) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_11; uint8_t x_12;
|
||||
x_11 = l_Lean_Elab_Tactic_Omega_evalOmega___closed__3;
|
||||
lean_inc(x_1);
|
||||
x_12 = l_Lean_Syntax_isOfKind(x_1, x_11);
|
||||
if (x_12 == 0)
|
||||
{
|
||||
lean_object* x_13;
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_13 = l_Lean_Elab_throwUnsupportedSyntax___at_Lean_MVarId_elabFalseOrByContra___spec__1___rarg(x_10);
|
||||
return x_13;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17;
|
||||
x_14 = lean_unsigned_to_nat(1u);
|
||||
x_15 = l_Lean_Syntax_getArg(x_1, x_14);
|
||||
lean_dec(x_1);
|
||||
x_16 = l_Lean_Elab_Tactic_Omega_evalOmega___closed__4;
|
||||
x_17 = l_Lean_Syntax_isNone(x_15);
|
||||
if (x_17 == 0)
|
||||
{
|
||||
uint8_t x_18;
|
||||
lean_inc(x_15);
|
||||
x_18 = l_Lean_Syntax_matchesNull(x_15, x_14);
|
||||
if (x_18 == 0)
|
||||
{
|
||||
lean_object* x_19;
|
||||
lean_dec(x_15);
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
x_19 = l_Lean_Elab_throwUnsupportedSyntax___at_Lean_MVarId_elabFalseOrByContra___spec__1___rarg(x_10);
|
||||
return x_19;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
|
||||
x_20 = lean_unsigned_to_nat(0u);
|
||||
x_21 = l_Lean_Syntax_getArg(x_15, x_20);
|
||||
lean_dec(x_15);
|
||||
x_22 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_22, 0, x_21);
|
||||
x_23 = lean_box(0);
|
||||
x_24 = lean_apply_11(x_16, x_23, x_22, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
|
||||
return x_24;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_25; lean_object* x_26; lean_object* x_27;
|
||||
lean_dec(x_15);
|
||||
x_25 = lean_box(0);
|
||||
x_26 = lean_box(0);
|
||||
x_27 = lean_apply_11(x_16, x_26, x_25, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
|
||||
return x_27;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_evalOmega___lambda__1___boxed(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) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_12;
|
||||
x_12 = l_Lean_Elab_Tactic_Omega_evalOmega___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
|
||||
lean_dec(x_1);
|
||||
return x_12;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__1() {
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -37619,7 +37397,7 @@ x_1 = lean_mk_string_unchecked("Elab", 4, 4);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__2() {
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -37627,20 +37405,20 @@ x_1 = lean_mk_string_unchecked("evalOmega", 9, 9);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__3() {
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__6() {
|
||||
_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;
|
||||
x_1 = l_Lean_Elab_Tactic_Omega_evalUnsafe____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_6____closed__1;
|
||||
x_2 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__1;
|
||||
x_3 = l_Lean_Elab_Tactic_Omega_evalOmega___closed__2;
|
||||
x_2 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__4;
|
||||
x_3 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__2;
|
||||
x_4 = l_Lean_Elab_Tactic_Omega_evalUnsafe____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_6____closed__3;
|
||||
x_5 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__2;
|
||||
x_5 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__5;
|
||||
x_6 = l_Lean_Name_mkStr5(x_1, x_2, x_3, x_4, x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__4() {
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__7() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -37648,11 +37426,11 @@ x_1 = l_Lean_Elab_Tactic_tacticElabAttribute;
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__5() {
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__8() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_Omega_evalOmega), 10, 0);
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_Omega_evalOmega___boxed), 10, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
|
|
@ -37660,10 +37438,10 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1(lean
|
|||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_2 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__4;
|
||||
x_3 = l_Lean_Elab_Tactic_Omega_evalOmega___closed__3;
|
||||
x_4 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__3;
|
||||
x_5 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__5;
|
||||
x_2 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__7;
|
||||
x_3 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__3;
|
||||
x_4 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__6;
|
||||
x_5 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__8;
|
||||
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
|
||||
return x_6;
|
||||
}
|
||||
|
|
@ -37764,13 +37542,13 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega_declRan
|
|||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_2 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__3;
|
||||
x_2 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__6;
|
||||
x_3 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega_declRange__1___closed__7;
|
||||
x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__1() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -37778,17 +37556,17 @@ x_1 = lean_mk_string_unchecked("bv_toNat", 8, 8);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__2() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__1;
|
||||
x_2 = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__1;
|
||||
x_3 = l_Lean_Name_str___override(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__3() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -37796,20 +37574,20 @@ x_1 = lean_mk_string_unchecked("bvOmegaSimpExtension", 20, 20);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__4() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__4() {
|
||||
_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;
|
||||
x_1 = l_Lean_Elab_Tactic_Omega_evalUnsafe____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_6____closed__1;
|
||||
x_2 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__1;
|
||||
x_3 = l_Lean_Elab_Tactic_Omega_evalOmega___closed__2;
|
||||
x_2 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__4;
|
||||
x_3 = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__2;
|
||||
x_4 = l_Lean_Elab_Tactic_Omega_evalUnsafe____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_6____closed__3;
|
||||
x_5 = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__3;
|
||||
x_5 = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__3;
|
||||
x_6 = l_Lean_Name_mkStr5(x_1, x_2, x_3, x_4, x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__5() {
|
||||
static lean_object* _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -37817,13 +37595,13 @@ x_1 = lean_mk_string_unchecked("simp lemmas converting `BitVec` goals to `Nat` g
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061_(lean_object* x_1) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967_(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_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__2;
|
||||
x_3 = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__5;
|
||||
x_4 = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__4;
|
||||
x_2 = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__2;
|
||||
x_3 = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__5;
|
||||
x_4 = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__4;
|
||||
x_5 = l_Lean_Meta_registerSimpAttr(x_2, x_3, x_4, x_1);
|
||||
return x_5;
|
||||
}
|
||||
|
|
@ -38809,16 +38587,6 @@ l_Lean_Elab_Tactic_Omega_omegaTactic___lambda__2___closed__3 = _init_l_Lean_Elab
|
|||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_omegaTactic___lambda__2___closed__3);
|
||||
l_Lean_Elab_Tactic_Omega_omegaTactic___lambda__2___closed__4 = _init_l_Lean_Elab_Tactic_Omega_omegaTactic___lambda__2___closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_omegaTactic___lambda__2___closed__4);
|
||||
l_Lean_Elab_Tactic_Omega_evalOmega___lambda__1___closed__1 = _init_l_Lean_Elab_Tactic_Omega_evalOmega___lambda__1___closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_evalOmega___lambda__1___closed__1);
|
||||
l_Lean_Elab_Tactic_Omega_evalOmega___closed__1 = _init_l_Lean_Elab_Tactic_Omega_evalOmega___closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_evalOmega___closed__1);
|
||||
l_Lean_Elab_Tactic_Omega_evalOmega___closed__2 = _init_l_Lean_Elab_Tactic_Omega_evalOmega___closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_evalOmega___closed__2);
|
||||
l_Lean_Elab_Tactic_Omega_evalOmega___closed__3 = _init_l_Lean_Elab_Tactic_Omega_evalOmega___closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_evalOmega___closed__3);
|
||||
l_Lean_Elab_Tactic_Omega_evalOmega___closed__4 = _init_l_Lean_Elab_Tactic_Omega_evalOmega___closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_evalOmega___closed__4);
|
||||
l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__1);
|
||||
l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__2();
|
||||
|
|
@ -38829,6 +38597,12 @@ l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__4 = _init_l___regBu
|
|||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__4);
|
||||
l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__5 = _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__5();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__5);
|
||||
l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__6 = _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__6();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__6);
|
||||
l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__7 = _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__7();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__7);
|
||||
l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__8 = _init_l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__8();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1___closed__8);
|
||||
if (builtin) {res = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega__1(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
|
|
@ -38849,17 +38623,17 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega_declRange__
|
|||
if (builtin) {res = l___regBuiltin_Lean_Elab_Tactic_Omega_evalOmega_declRange__1(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
}l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__1 = _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__1);
|
||||
l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__2 = _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__2);
|
||||
l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__3 = _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__3);
|
||||
l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__4 = _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__4);
|
||||
l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__5 = _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__5();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061____closed__5);
|
||||
if (builtin) {res = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_16061_(lean_io_mk_world());
|
||||
}l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__1 = _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__1);
|
||||
l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__2 = _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__2);
|
||||
l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__3 = _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__3);
|
||||
l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__4 = _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__4);
|
||||
l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__5 = _init_l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__5();
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967____closed__5);
|
||||
if (builtin) {res = l_Lean_Elab_Tactic_Omega_initFn____x40_Lean_Elab_Tactic_Omega_Frontend___hyg_15967_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
l_Lean_Elab_Tactic_Omega_bvOmegaSimpExtension = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_Elab_Tactic_Omega_bvOmegaSimpExtension);
|
||||
|
|
|
|||
1196
stage0/stdlib/Lean/Elab/Tactic/SolveByElim.c
generated
1196
stage0/stdlib/Lean/Elab/Tactic/SolveByElim.c
generated
File diff suppressed because it is too large
Load diff
521
stage0/stdlib/Lean/Environment.c
generated
521
stage0/stdlib/Lean/Environment.c
generated
File diff suppressed because it is too large
Load diff
2
stage0/stdlib/Lean/Server/Watchdog.c
generated
2
stage0/stdlib/Lean/Server/Watchdog.c
generated
|
|
@ -7137,7 +7137,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;
|
||||
x_1 = l_Lean_RBNode_forIn_visit___at_Lean_Server_Watchdog_ImportData_update___spec__11___closed__1;
|
||||
x_2 = l_Lean_RBNode_forIn_visit___at_Lean_Server_Watchdog_ImportData_update___spec__11___closed__2;
|
||||
x_3 = lean_unsigned_to_nat(384u);
|
||||
x_3 = lean_unsigned_to_nat(389u);
|
||||
x_4 = lean_unsigned_to_nat(14u);
|
||||
x_5 = l_Lean_RBNode_forIn_visit___at_Lean_Server_Watchdog_ImportData_update___spec__11___closed__3;
|
||||
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue