diff --git a/stage0/stdlib/Lean/Compiler/InitAttr.c b/stage0/stdlib/Lean/Compiler/InitAttr.c index f815088f5e..cd7e4f4c97 100644 --- a/stage0/stdlib/Lean/Compiler/InitAttr.c +++ b/stage0/stdlib/Lean/Compiler/InitAttr.c @@ -13,7 +13,6 @@ #ifdef __cplusplus extern "C" { #endif -static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__1; lean_object* l_Lean_addMessageContextPartial___at_Lean_Core_instAddMessageContextCoreM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_registerInitAttrUnsafe___spec__2(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_registerInitAttrUnsafe(lean_object*, uint8_t, lean_object*); @@ -40,12 +39,12 @@ static lean_object* l_Lean_getConstInfo___at_Lean_registerInitAttrUnsafe___spec_ static lean_object* l_Lean_declareBuiltin___closed__5; static lean_object* l_Lean_setEnv___at_Lean_declareBuiltin___spec__3___closed__4; lean_object* l_List_filterMap___at_Lean_resolveGlobalConst___spec__1(lean_object*); -static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__2; static lean_object* l_Lean_declareBuiltin___closed__3; LEAN_EXPORT uint8_t lean_is_io_unit_regular_init_fn(lean_object*, lean_object*); lean_object* lean_environment_find(lean_object*, lean_object*); static lean_object* l_Lean_registerInitAttrUnsafe___closed__3; lean_object* lean_st_ref_get(lean_object*, lean_object*); +static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__2; LEAN_EXPORT lean_object* l_Lean_resolveGlobalName___at_Lean_registerInitAttrUnsafe___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_declareBuiltin___closed__9; LEAN_EXPORT lean_object* l_Lean_getConstInfo___at_Lean_registerInitAttrUnsafe___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); @@ -57,6 +56,7 @@ static lean_object* l_Lean_declareBuiltin___closed__8; static lean_object* l_Lean_registerInitAttrUnsafe___lambda__1___closed__6; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_registerInitAttrUnsafe___spec__13(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_registerInitAttrUnsafe___boxed(lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__1; lean_object* lean_run_mod_init(lean_object*, lean_object*); static lean_object* l_Lean_registerInitAttrUnsafe___closed__2; LEAN_EXPORT lean_object* l_Lean_throwUnknownConstant___at_Lean_registerInitAttrUnsafe___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -69,8 +69,8 @@ LEAN_EXPORT lean_object* l_Lean_registerInitAttrUnsafe___lambda__3___boxed(lean_ lean_object* l_List_mapTRAux___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_registerInitAttrUnsafe___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_resolveGlobalName___at_Lean_registerInitAttrUnsafe___spec__9(lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798_(lean_object*); -LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819_(lean_object*); LEAN_EXPORT lean_object* l_Lean_resolveGlobalConst___at_Lean_registerInitAttrUnsafe___spec__5(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_array_fget(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstCore___at_Lean_registerInitAttrUnsafe___spec__8___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -87,9 +87,9 @@ LEAN_EXPORT lean_object* l_Lean_registerInitAttrUnsafe___lambda__1(lean_object*, lean_object* l_Lean_KernelException_toMessageData(lean_object*, lean_object*); static lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_registerInitAttrUnsafe___spec__4___closed__1; lean_object* l_Lean_replaceRef(lean_object*, lean_object*); +static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__2; static lean_object* l_Lean_declareBuiltin___closed__2; static lean_object* l_Lean_declareBuiltin___closed__12; -static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__2; LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_registerInitAttrUnsafe___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_registerInitAttrUnsafe___spec__4___closed__2; lean_object* l_Lean_isInitializerExecutionEnabled(lean_object*); @@ -110,9 +110,9 @@ lean_object* lean_eval_const(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_hasInitAttr___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* lean_get_regular_init_fn_name_for(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_declareBuiltin___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__1; LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_registerInitAttrUnsafe___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_getConstInfo___at_Lean_registerInitAttrUnsafe___spec__1___closed__4; +static lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__1; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_registerInitAttrUnsafe___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_registerInitAttrUnsafe___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*); @@ -2375,7 +2375,7 @@ x_5 = l_Lean_registerInitAttrUnsafe(x_1, x_4, x_3); return x_5; } } -static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__1() { +static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__1() { _start: { lean_object* x_1; @@ -2383,27 +2383,27 @@ x_1 = lean_mk_string_from_bytes("init", 4); return x_1; } } -static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__2() { +static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__1; +x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802_(lean_object* x_1) { _start: { lean_object* x_2; uint8_t x_3; lean_object* x_4; -x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__2; +x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__2; x_3 = 1; x_4 = l_Lean_registerInitAttrUnsafe(x_2, x_3, x_1); return x_4; } } -static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__1() { +static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__1() { _start: { lean_object* x_1; @@ -2411,21 +2411,21 @@ x_1 = lean_mk_string_from_bytes("builtinInit", 11); return x_1; } } -static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__2() { +static lean_object* _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__1; +x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819_(lean_object* x_1) { _start: { lean_object* x_2; uint8_t x_3; lean_object* x_4; -x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__2; +x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__2; x_3 = 0; x_4 = l_Lean_registerInitAttrUnsafe(x_2, x_3, x_1); return x_4; @@ -3316,20 +3316,20 @@ l_Lean_registerInitAttrUnsafe___closed__2 = _init_l_Lean_registerInitAttrUnsafe_ lean_mark_persistent(l_Lean_registerInitAttrUnsafe___closed__2); l_Lean_registerInitAttrUnsafe___closed__3 = _init_l_Lean_registerInitAttrUnsafe___closed__3(); lean_mark_persistent(l_Lean_registerInitAttrUnsafe___closed__3); -l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__1 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__1(); -lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__1); -l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__2 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__2(); -lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798____closed__2); -if (builtin) {res = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_798_(lean_io_mk_world()); +l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__1 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__1(); +lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__1); +l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__2 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__2(); +lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802____closed__2); +if (builtin) {res = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_802_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_regularInitAttr = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_regularInitAttr); lean_dec_ref(res); -}l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__1 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__1(); -lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__1); -l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__2 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__2(); -lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815____closed__2); -if (builtin) {res = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_815_(lean_io_mk_world()); +}l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__1 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__1(); +lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__1); +l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__2 = _init_l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__2(); +lean_mark_persistent(l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819____closed__2); +if (builtin) {res = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_819_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_builtinInitAttr = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_builtinInitAttr); diff --git a/stage0/stdlib/Lean/Elab/Binders.c b/stage0/stdlib/Lean/Elab/Binders.c index b4908a6bd2..c2b9817f3b 100644 --- a/stage0/stdlib/Lean/Elab/Binders.c +++ b/stage0/stdlib/Lean/Elab/Binders.c @@ -329,7 +329,7 @@ lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_expandFunBinders_loop___spec__4(lean_object*, size_t, size_t, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Term_elabLetTmpDecl___closed__4; static lean_object* l___regBuiltin_Lean_Elab_Term_expandFun_declRange___closed__4; -LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_7537_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_7541_(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_1498_(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Term_elabDepArrow___closed__4; LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__6(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -29559,7 +29559,7 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1); return x_4; } } -LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_7537_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_7541_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -30363,7 +30363,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabLetTmpDecl_declRange___cl res = l___regBuiltin_Lean_Elab_Term_elabLetTmpDecl_declRange(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_7537_(lean_io_mk_world()); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Binders___hyg_7541_(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)); diff --git a/stage0/stdlib/Lean/Elab/Deriving/Basic.c b/stage0/stdlib/Lean/Elab/Deriving/Basic.c index cb8bc9efe3..fd2fcfbe28 100644 --- a/stage0/stdlib/Lean/Elab/Deriving/Basic.c +++ b/stage0/stdlib/Lean/Elab/Deriving/Basic.c @@ -26,16 +26,16 @@ LEAN_EXPORT lean_object* l_Lean_Elab_registerBuiltinDerivingHandlerWithArgs___la lean_object* lean_mk_empty_array_with_capacity(lean_object*); LEAN_EXPORT lean_object* l_Lean_getConstInfo___at_Lean_Elab_elabDeriving___spec__14(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_filterTRAux___at_Lean_resolveGlobalConstCore___spec__1(lean_object*, lean_object*); -static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__2; lean_object* l_Lean_Elab_Command_liftTermElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_name_mk_string(lean_object*, lean_object*); static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_elabDeriving___spec__12___closed__2; lean_object* lean_array_uget(lean_object*, size_t); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_getOptDerivingClasses___spec__1(lean_object*); -static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__1; static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_elabDeriving___spec__1___rarg___closed__2; lean_object* l_List_mapTRAux___at_Lean_resolveGlobalConstCore___spec__2(lean_object*, lean_object*); extern lean_object* l_Std_Format_defWidth; +static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__1; +static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__2; LEAN_EXPORT lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_elabDeriving___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_elabDeriving_declRange___closed__7; LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_elabDeriving___spec__15___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -100,7 +100,7 @@ lean_object* lean_st_ref_take(lean_object*, lean_object*); static lean_object* l_Lean_Elab_elabDeriving___closed__2; lean_object* lean_nat_sub(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_elabDeriving___spec__1(lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527_(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_25_(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_elabDeriving_declRange___closed__5; LEAN_EXPORT lean_object* l_Lean_Elab_registerBuiltinDerivingHandler___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -148,6 +148,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_pushInfoTree___at_Lean_Elab_elabDeriving___ LEAN_EXPORT lean_object* l_Lean_Elab_elabDeriving___lambda__1(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_elabDeriving___lambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*); +static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__3; LEAN_EXPORT lean_object* l_Lean_Elab_elabDeriving___lambda__3(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_getOptDerivingClasses___rarg___lambda__1(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Deriving_Basic_0__Lean_Elab_tryApplyDefHandler___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -166,7 +167,6 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_elabDeriving___sp LEAN_EXPORT lean_object* l_Lean_Elab_defaultHandler(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_elabDeriving___spec__8___closed__3; LEAN_EXPORT lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_elabDeriving___spec__16(lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__3; lean_object* l_Lean_Elab_Term_processDefDeriving(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_mapTRAux___at_Lean_mkConstWithLevelParams___spec__1(lean_object*, lean_object*); @@ -4485,7 +4485,7 @@ return x_24; } } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__1() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -4495,7 +4495,7 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__2() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__2() { _start: { lean_object* x_1; @@ -4503,21 +4503,21 @@ x_1 = lean_mk_string_from_bytes("Deriving", 8); return x_1; } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__3() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__1; -x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__2; +x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__1; +x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__2; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__3; +x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__3; x_3 = l_Lean_registerTraceClass(x_2, x_1); return x_3; } @@ -4656,13 +4656,13 @@ l_Lean_Elab_getOptDerivingClasses___rarg___closed__1 = _init_l_Lean_Elab_getOptD lean_mark_persistent(l_Lean_Elab_getOptDerivingClasses___rarg___closed__1); l_Lean_Elab_getOptDerivingClasses___rarg___closed__2 = _init_l_Lean_Elab_getOptDerivingClasses___rarg___closed__2(); lean_mark_persistent(l_Lean_Elab_getOptDerivingClasses___rarg___closed__2); -l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__1(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__1); -l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__2(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__2); -l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__3(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519____closed__3); -res = l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1519_(lean_io_mk_world()); +l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__1(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__1); +l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__2(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__2); +l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__3(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527____closed__3); +res = l_Lean_Elab_initFn____x40_Lean_Elab_Deriving_Basic___hyg_1527_(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)); diff --git a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c index fa042b92f4..ebe24edbe1 100644 --- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c +++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c @@ -29,7 +29,7 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Structural_str LEAN_EXPORT lean_object* l_Lean_setEnv___at___private_Lean_Elab_PreDefinition_Structural_Main_0__Lean_Elab_Structural_elimRecursion___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Structural_structuralRecursion(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_PreDefinition_Structural_Main_0__Lean_Elab_Structural_elimRecursion___lambda__6___closed__3; -LEAN_EXPORT lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Main___hyg_1093_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Main___hyg_1097_(lean_object*); static lean_object* l_Lean_setEnv___at___private_Lean_Elab_PreDefinition_Structural_Main_0__Lean_Elab_Structural_elimRecursion___spec__2___closed__10; static lean_object* l_Lean_Elab_Structural_structuralRecursion___lambda__1___closed__1; static lean_object* l_Lean_setEnv___at___private_Lean_Elab_PreDefinition_Structural_Main_0__Lean_Elab_Structural_elimRecursion___spec__2___closed__9; @@ -3223,7 +3223,7 @@ lean_dec(x_1); return x_9; } } -LEAN_EXPORT lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Main___hyg_1093_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Main___hyg_1097_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -3349,7 +3349,7 @@ l_Lean_Elab_Structural_structuralRecursion___closed__4 = _init_l_Lean_Elab_Struc lean_mark_persistent(l_Lean_Elab_Structural_structuralRecursion___closed__4); l_Lean_Elab_Structural_structuralRecursion___closed__5 = _init_l_Lean_Elab_Structural_structuralRecursion___closed__5(); lean_mark_persistent(l_Lean_Elab_Structural_structuralRecursion___closed__5); -res = l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Main___hyg_1093_(lean_io_mk_world()); +res = l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural_Main___hyg_1097_(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)); diff --git a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c index 00237dd0e9..6471a0cf0a 100644 --- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c +++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c @@ -108,7 +108,7 @@ static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_wfRecursion___spec__3_ lean_object* l_Lean_Meta_lambdaTelescope___at_Lean_Meta_CasesOnApp_addArg___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_mk_ref(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2114_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2118_(lean_object*); static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs_mkSum___spec__1___closed__10; static lean_object* l_Lean_Elab_wfRecursion___closed__5; LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs___spec__1___lambda__2(lean_object*, uint8_t, 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*); @@ -5610,7 +5610,7 @@ lean_dec(x_5); return x_15; } } -LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2114_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2118_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -5752,7 +5752,7 @@ l_Lean_Elab_wfRecursion___closed__5 = _init_l_Lean_Elab_wfRecursion___closed__5( lean_mark_persistent(l_Lean_Elab_wfRecursion___closed__5); l_Lean_Elab_wfRecursion___closed__6 = _init_l_Lean_Elab_wfRecursion___closed__6(); lean_mark_persistent(l_Lean_Elab_wfRecursion___closed__6); -res = l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2114_(lean_io_mk_world()); +res = l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2118_(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)); diff --git a/stage0/stdlib/Lean/Meta/Injective.c b/stage0/stdlib/Lean/Meta/Injective.c index 94217d740c..1acc80d5a9 100644 --- a/stage0/stdlib/Lean/Meta/Injective.c +++ b/stage0/stdlib/Lean/Meta/Injective.c @@ -26,7 +26,6 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*); lean_object* l_Lean_Meta_mkForallFVars(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_injTheoremFailureHeader___closed__4; lean_object* lean_name_mk_string(lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__1; lean_object* lean_array_uget(lean_object*, size_t); LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_panic___at___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___spec__1___closed__1; @@ -36,10 +35,10 @@ LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkInjectiveTheorems___ LEAN_EXPORT lean_object* l_Lean_Meta_elimOptParam___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_injTheoremFailureHeader___closed__3; static lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Meta_Injective_0__Lean_Meta_mkAnd_x3f___spec__1___closed__1; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__2; lean_object* l_Lean_Meta_addSimpTheorem(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_elimOptParam___lambda__1___closed__2; LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Meta_Injective_0__Lean_Meta_mkAnd_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__4; LEAN_EXPORT lean_object* l_Lean_Meta_mkInjectiveTheorems(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkInjectiveTheorems___closed__1; lean_object* lean_st_ref_get(lean_object*, lean_object*); @@ -58,7 +57,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_elimOptParam(lean_object*, lean_object*, le static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_throwInjectiveTheoremFailure___rarg___closed__1; static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_elimOptParam___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__2; lean_object* l_Lean_Expr_getRevArg_x21(lean_object*, lean_object*); static lean_object* l_Lean_Meta_elimOptParam___lambda__1___closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_withNewBinderInfos___at___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___spec__3(lean_object*); @@ -96,9 +94,9 @@ lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint lean_object* l_Lean_Expr_fvarId_x21(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f_mkArgs2(lean_object*, uint8_t, 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___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f_mkArgs2___closed__3; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__3; LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_Injective_0__Lean_Meta_throwInjectiveTheoremFailure___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__3; static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_injTheoremFailureHeader___closed__2; lean_object* l_Array_back___rarg(lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheorem___closed__1; @@ -121,7 +119,9 @@ static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTh size_t lean_usize_of_nat(lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___spec__2(size_t, size_t, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheoremValue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_withNewBinderInfos___at___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__4; LEAN_EXPORT lean_object* l_List_forM___at___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheoremValue___lambda__2___closed__3; @@ -135,7 +135,7 @@ static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTh lean_object* l_Lean_Meta_substEqs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*); lean_object* l_Lean_Meta_assumptionCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649_(lean_object*); uint8_t lean_expr_eqv(lean_object*, lean_object*); lean_object* l_Lean_throwError___at_Lean_Meta_abstractRange___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_mkInjectiveTheoremNameFor___boxed(lean_object*); @@ -3972,7 +3972,7 @@ return x_87; } } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__1() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__1() { _start: { lean_object* x_1; @@ -3980,17 +3980,17 @@ x_1 = lean_mk_string_from_bytes("genInjectivity", 14); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__2() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__1; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__3() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__3() { _start: { lean_object* x_1; @@ -3998,13 +3998,13 @@ x_1 = lean_mk_string_from_bytes("generate injectivity theorems for inductive dat return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__4() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__4() { _start: { uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = 1; x_2 = l___private_Lean_Meta_Injective_0__Lean_Meta_throwInjectiveTheoremFailure___rarg___closed__1; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__3; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__3; x_4 = lean_box(x_1); x_5 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_5, 0, x_4); @@ -4013,12 +4013,12 @@ lean_ctor_set(x_5, 2, x_3); return x_5; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__2; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__4; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__2; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__4; x_4 = l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hyg_54____spec__1(x_2, x_3, x_1); return x_4; } @@ -4746,15 +4746,15 @@ l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheoremValue___lambda_ lean_mark_persistent(l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheoremValue___lambda__2___closed__7); l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheorem___closed__1 = _init_l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheorem___closed__1(); lean_mark_persistent(l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheorem___closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__1(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__2(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__3(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__3); -l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__4(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645____closed__4); -if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1645_(lean_io_mk_world()); +l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__1(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__1); +l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__2(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__2); +l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__3(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__3); +l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__4(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649____closed__4); +if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1649_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Meta_genInjectivity = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Meta_genInjectivity); diff --git a/stage0/stdlib/Lean/Meta/Match/Match.c b/stage0/stdlib/Lean/Meta/Match/Match.c index 3757921859..a32764021e 100644 --- a/stage0/stdlib/Lean/Meta/Match/Match.c +++ b/stage0/stdlib/Lean/Meta/Match/Match.c @@ -291,7 +291,7 @@ static lean_object* l_List_filterMapM_loop___at___private_Lean_Meta_Match_Match_ uint8_t l_Array_contains___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___spec__3(lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___closed__3; size_t lean_uint64_to_usize(uint64_t); -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_13844_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_13848_(lean_object*); lean_object* l_Lean_Expr_FindImpl_findUnsafe_x3f(lean_object*, lean_object*); uint8_t l_Lean_Environment_hasUnsafe(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_checkNextPatternTypes(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -35853,7 +35853,7 @@ return x_21; } } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_13844_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_13848_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -36503,7 +36503,7 @@ l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__3 = _init_l_Lean_Meta_Matche lean_mark_persistent(l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__3); l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__4 = _init_l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__4(); lean_mark_persistent(l_Lean_Meta_MatcherApp_addArg___lambda__4___closed__4); -res = l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_13844_(lean_io_mk_world()); +res = l_Lean_Meta_initFn____x40_Lean_Meta_Match_Match___hyg_13848_(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)); diff --git a/stage0/stdlib/Lean/Meta/Match/MatchEqs.c b/stage0/stdlib/Lean/Meta/Match/MatchEqs.c index 61d8e2c572..8255923ebc 100644 --- a/stage0/stdlib/Lean/Meta/Match/MatchEqs.c +++ b/stage0/stdlib/Lean/Meta/Match/MatchEqs.c @@ -523,7 +523,7 @@ LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_M uint8_t lean_expr_eqv(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_withIncRecDepth___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertTemplate___spec__18(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___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_simpH_x3f___closed__3; -LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_MatchEqs___hyg_11783_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_MatchEqs___hyg_11803_(lean_object*); static lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop___lambda__1___closed__3; lean_object* l_Lean_throwError___at_Lean_Meta_abstractRange___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertCastEqRec___spec__6___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -34682,7 +34682,7 @@ lean_dec(x_3); return x_5; } } -LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_MatchEqs___hyg_11783_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_MatchEqs___hyg_11803_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -35145,7 +35145,7 @@ l_Std_PersistentHashMap_findAux___at_Lean_Meta_Match_getEquationsForImpl___spec_ l_Std_PersistentHashMap_findAux___at_Lean_Meta_Match_getEquationsForImpl___spec__2___closed__2 = _init_l_Std_PersistentHashMap_findAux___at_Lean_Meta_Match_getEquationsForImpl___spec__2___closed__2(); l_Lean_Meta_Match_getEquationsForImpl___closed__1 = _init_l_Lean_Meta_Match_getEquationsForImpl___closed__1(); lean_mark_persistent(l_Lean_Meta_Match_getEquationsForImpl___closed__1); -res = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_MatchEqs___hyg_11783_(lean_io_mk_world()); +res = l_Lean_Meta_Match_initFn____x40_Lean_Meta_Match_MatchEqs___hyg_11803_(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)); diff --git a/stage0/stdlib/Lean/Meta/SizeOf.c b/stage0/stdlib/Lean/Meta/SizeOf.c index c117f8435c..1c72e9d8a6 100644 --- a/stage0/stdlib/Lean/Meta/SizeOf.c +++ b/stage0/stdlib/Lean/Meta/SizeOf.c @@ -15,7 +15,6 @@ extern "C" { #endif LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_mkSizeOfSpecLemmaInstance___spec__1___boxed(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___spec__2___closed__2; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__4; static lean_object* l_Lean_Meta_mkSizeOfFn___lambda__2___closed__1; size_t lean_usize_add(size_t, size_t); lean_object* l_List_tail_x21___rarg(lean_object*); @@ -35,11 +34,13 @@ static lean_object* l_Lean_Meta_SizeOfSpecNested_main_loop___closed__1; lean_object* l_Lean_RecursorVal_getFirstIndexIdx(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_mkSizeOfSpecLemmaName(lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkSizeOfFns___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__4; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_SizeOf_0__Lean_Meta_isRecField_x3f___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* l_Lean_throwError___at_Lean_Meta_setInlineAttribute___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_name_mk_string(lean_object*, lean_object*); uint8_t lean_usize_dec_eq(size_t, size_t); lean_object* lean_array_uget(lean_object*, size_t); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__3; static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkLocalInstances_loop___rarg___closed__2; lean_object* l_Lean_Expr_bindingDomain_x21(lean_object*); lean_object* l_Array_append___rarg(lean_object*, lean_object*); @@ -84,7 +85,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNes LEAN_EXPORT lean_object* l_Lean_logAt___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___spec__7(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Expr_isApp(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SizeOfSpecNested_main_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__3; LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_recToSizeOf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SizeOfSpecNested_main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Array_contains___at___private_Lean_Meta_SizeOf_0__Lean_Meta_isInductiveHypothesis_x3f___spec__1(lean_object*, lean_object*); @@ -151,7 +151,6 @@ static lean_object* l_Lean_addTrace___at___private_Lean_Meta_SizeOf_0__Lean_Meta LEAN_EXPORT lean_object* l_Lean_getConstInfoInduct___at_Lean_Meta_mkSizeOfFns___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_genSizeOfSpec; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__1; LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_mkSizeOfSpecLemmaInstance___spec__1(size_t, size_t, lean_object*); static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___rarg___closed__3; @@ -166,7 +165,6 @@ static lean_object* l_Lean_setEnv___at___private_Lean_Meta_SizeOf_0__Lean_Meta_S uint8_t lean_nat_dec_eq(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof_mkSizeOf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkSizeOfFns___closed__3; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__2; lean_object* lean_st_ref_take(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_mkSizeOfFn___lambda__5___boxed(lean_object**); lean_object* lean_nat_sub(lean_object*, lean_object*); @@ -186,6 +184,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNes LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Meta_SizeOf_0__Lean_Meta_isInductiveHypothesis_x3f___spec__2(lean_object*, lean_object*, size_t, size_t); lean_object* l_Lean_KernelException_toMessageData(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkLocalInstances___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_mkSizeOfSpecLemmaInstance(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___lambda__2___closed__1; @@ -215,6 +214,7 @@ static lean_object* l_panic___at___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeO lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__1; LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors_loop___rarg___lambda__2(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___private_Lean_Meta_SizeOf_0__Lean_Meta_isRecField_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_setEnv___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___spec__5___closed__4; @@ -265,7 +265,6 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_SizeOf_0__Le static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___rarg___closed__6; uint8_t l_Lean_MessageData_hasSyntheticSorry(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_mkSizeOfSpecLemmaName___boxed(lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__4; LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___lambda__2___boxed__const__1; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___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*, lean_object*); uint8_t l_Lean_Expr_isForall(lean_object*); @@ -350,6 +349,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_ static lean_object* l_Lean_Meta_mkSizeOfFns___closed__4; static lean_object* l_Lean_setEnv___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___spec__5___closed__12; lean_object* l_Lean_Meta_unfoldDefinition(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__4; static lean_object* l_Lean_addTrace___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___spec__1___closed__6; lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_SynthInstance_removeUnusedArguments_x3f___spec__2___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors_loop___rarg___lambda__2___closed__1; @@ -412,9 +412,9 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_isInductiveHy LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkLocalInstances(lean_object*); lean_object* l_Lean_getConstInfoCtor___at___private_Lean_Meta_WHNF_0__Lean_Meta_toCtorWhenStructure___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_lengthTRAux___rarg(lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6721_(lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161_(lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6729_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188_(lean_object*); LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___spec__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_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_SizeOfSpecNested_throwFailed___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__1; @@ -427,6 +427,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecT lean_object* l_Lean_Expr_getAppFn(lean_object*); static lean_object* l_Lean_addTrace___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___spec__1___closed__1; static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___rarg___closed__1; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__3; LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_isInductiveHypothesis_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___lambda__1___closed__5; uint8_t l_Std_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_object*); @@ -439,7 +440,6 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_SizeO extern lean_object* l_Lean_levelOne; lean_object* l_Lean_Meta_mkEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__3; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__3; lean_object* l_Lean_indentExpr(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMotives_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___rarg___closed__4; @@ -453,9 +453,9 @@ static lean_object* l_Lean_Meta_mkSizeOfSpecLemmaName___closed__2; LEAN_EXPORT lean_object* l_Lean_addTrace___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_forIn_loop___at___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorems___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_ignoreField(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__1; static lean_object* l_Lean_Meta_mkSizeOfInstances___closed__2; static lean_object* l_Lean_addTrace___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___spec__1___closed__2; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__2; lean_object* l_Lean_getAttributeImpl(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___lambda__2(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_object*); static lean_object* l_Lean_Meta_mkSizeOfSpecLemmaName___closed__1; @@ -468,12 +468,12 @@ static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1 lean_object* l_Lean_Meta_instInhabitedMetaM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkAdd(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkSizeOfSpecLemmaInstance___closed__2; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__1; LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkNumeral(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___lambda__2___closed__1; static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfRecFieldFormIH___closed__1; static lean_object* l_Lean_setEnv___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___spec__5___closed__7; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__2; LEAN_EXPORT lean_object* l_Lean_getConstInfoInduct___at_Lean_Meta_mkSizeOfFns___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_addTrace___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -17014,7 +17014,7 @@ lean_dec(x_1); return x_9; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__1() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__1() { _start: { lean_object* x_1; @@ -17022,17 +17022,17 @@ x_1 = lean_mk_string_from_bytes("genSizeOf", 9); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__2() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__1; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__3() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__3() { _start: { lean_object* x_1; @@ -17040,13 +17040,13 @@ x_1 = lean_mk_string_from_bytes("generate `SizeOf` instance for inductive types return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__4() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__4() { _start: { uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = 1; x_2 = l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMotives_loop___rarg___closed__8; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__3; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__3; x_4 = lean_box(x_1); x_5 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_5, 0, x_4); @@ -17055,17 +17055,17 @@ lean_ctor_set(x_5, 2, x_3); return x_5; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__2; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__4; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__2; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__4; x_4 = l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hyg_54____spec__1(x_2, x_3, x_1); return x_4; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__1() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__1() { _start: { lean_object* x_1; @@ -17073,17 +17073,17 @@ x_1 = lean_mk_string_from_bytes("genSizeOfSpec", 13); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__2() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__1; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__3() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__3() { _start: { lean_object* x_1; @@ -17091,13 +17091,13 @@ x_1 = lean_mk_string_from_bytes("generate `SizeOf` specificiation theorems for a return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__4() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__4() { _start: { uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = 1; x_2 = l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMotives_loop___rarg___closed__8; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__3; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__3; x_4 = lean_box(x_1); x_5 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_5, 0, x_4); @@ -17106,12 +17106,12 @@ lean_ctor_set(x_5, 2, x_3); return x_5; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__2; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__4; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__2; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__4; x_4 = l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hyg_54____spec__1(x_2, x_3, x_1); return x_4; } @@ -18530,7 +18530,7 @@ lean_dec(x_7); return x_13; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6721_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6729_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -18800,28 +18800,28 @@ l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___closed__1 = _ini lean_mark_persistent(l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___closed__1); l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___closed__2 = _init_l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___closed__2(); lean_mark_persistent(l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__1(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__2(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__3(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__3); -l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__4(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161____closed__4); -if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6161_(lean_io_mk_world()); +l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__1(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__1); +l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__2(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__2); +l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__3(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__3); +l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__4(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165____closed__4); +if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6165_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Meta_genSizeOf = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Meta_genSizeOf); lean_dec_ref(res); -}l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__1(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__2(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__3(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__3); -l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__4(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184____closed__4); -if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6184_(lean_io_mk_world()); +}l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__1(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__1); +l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__2(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__2); +l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__3(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__3); +l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__4(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188____closed__4); +if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6188_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Meta_genSizeOfSpec = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Meta_genSizeOfSpec); @@ -18840,7 +18840,7 @@ l_Lean_Meta_mkSizeOfInstances___closed__1 = _init_l_Lean_Meta_mkSizeOfInstances_ lean_mark_persistent(l_Lean_Meta_mkSizeOfInstances___closed__1); l_Lean_Meta_mkSizeOfInstances___closed__2 = _init_l_Lean_Meta_mkSizeOfInstances___closed__2(); lean_mark_persistent(l_Lean_Meta_mkSizeOfInstances___closed__2); -res = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6721_(lean_io_mk_world()); +res = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6729_(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)); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Contradiction.c b/stage0/stdlib/Lean/Meta/Tactic/Contradiction.c index 36abfdcfe8..9d1f16cd56 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Contradiction.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Contradiction.c @@ -220,7 +220,7 @@ lean_object* l_Lean_Meta_mkFalseElim(lean_object*, lean_object*, lean_object*, l lean_object* l_Lean_Meta_mkNoConfusion(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Expr_hasLooseBVars(lean_object*); LEAN_EXPORT uint8_t l_Lean_Meta_Contradiction_Config_emptyType___default; -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Contradiction___hyg_4066_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Contradiction___hyg_4070_(lean_object*); lean_object* lean_mk_array(lean_object*, lean_object*); lean_object* l_panic___at_Lean_Meta_ACLt_lt_lexSameCtor___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Contradiction_0__Lean_Meta_mkGenDiseqMask___boxed(lean_object*); @@ -9907,7 +9907,7 @@ return x_24; } } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Contradiction___hyg_4066_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Contradiction___hyg_4070_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -10070,7 +10070,7 @@ l_Lean_Meta_contradiction___closed__1 = _init_l_Lean_Meta_contradiction___closed lean_mark_persistent(l_Lean_Meta_contradiction___closed__1); l_Lean_Meta_contradiction___closed__2 = _init_l_Lean_Meta_contradiction___closed__2(); lean_mark_persistent(l_Lean_Meta_contradiction___closed__2); -res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Contradiction___hyg_4066_(lean_io_mk_world()); +res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Contradiction___hyg_4070_(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)); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpCongrTheorems.c b/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpCongrTheorems.c index d5565468fd..90fbf12407 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpCongrTheorems.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpCongrTheorems.c @@ -17,6 +17,7 @@ lean_object* l_List_reverse___rarg(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51_(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at_Lean_Meta_mkSimpCongrTheorem___spec__11___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_object* lean_array_set(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_SimpCongrTheorems_lemmas___default___spec__1___boxed(lean_object*); static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpCongrTheorem___spec__1___closed__3; size_t lean_usize_add(size_t, size_t); @@ -27,7 +28,6 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem__ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__4___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_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__7___closed__1; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__9; lean_object* l_Lean_CollectMVars_visit(lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____closed__9; lean_object* l_Lean_stringToMessageData(lean_object*); @@ -41,11 +41,13 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem__ lean_object* l___private_Std_Data_HashMap_0__Std_numBucketsForCapacity(lean_object*); static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__4___closed__2; static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpCongrTheorem___spec__1___closed__5; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__8; LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkSimpCongrTheorem___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_name_mk_string(lean_object*, lean_object*); uint8_t lean_usize_dec_eq(size_t, size_t); lean_object* lean_array_uget(lean_object*, size_t); LEAN_EXPORT lean_object* l_Lean_Meta_instInhabitedSimpCongrTheorems; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__4; static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__6___closed__4; static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpCongrTheorem___spec__1___closed__1; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -58,16 +60,13 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem__ lean_object* l_Lean_throwError___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_registerSimpleScopedEnvExtension___rarg(lean_object*, lean_object*); lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_getParamNames___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__1; LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__9(lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__20; LEAN_EXPORT lean_object* l_Std_AssocList_contains___at_Lean_Meta_addSimpCongrTheoremEntry___spec__7___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__6(lean_object*); LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlM___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__11___rarg(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkSimpCongrTheorem___closed__1; -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_SimpCongrTheorems_lemmas___default___closed__1; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__2; size_t lean_usize_sub(size_t, size_t); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__23; LEAN_EXPORT lean_object* l_Std_HashMapImp_moveEntries___at_Lean_Meta_addSimpCongrTheoremEntry___spec__9(lean_object*, lean_object*, lean_object*); @@ -77,6 +76,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheo LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__5(lean_object*, lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentHashMap_foldlMAux_traverse___at_Lean_MetavarContext_getExprAssignmentDomain___spec__4___rarg(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_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__1; lean_object* l_Lean_Name_reprPrec(lean_object*, lean_object*); uint8_t lean_name_eq(lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__21; @@ -100,6 +100,7 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tact lean_object* l_Std_RBNode_findCore___at___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimApp___spec__5(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__2(lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__10___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__9; lean_object* l_Std_Format_joinSep___at_instReprProd___spec__1(lean_object*, lean_object*); lean_object* l_Std_mkHashSetImp___rarg(lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___at_Lean_Meta_mkSimpCongrTheorem___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -113,6 +114,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheo LEAN_EXPORT uint8_t l_Std_AssocList_contains___at_Lean_Meta_addSimpCongrTheoremEntry___spec__7(lean_object*, lean_object*); uint8_t lean_usize_dec_lt(size_t, size_t); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____closed__13; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__2; extern lean_object* l_Lean_levelZero; LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); @@ -129,13 +131,12 @@ static size_t l_Std_PersistentHashMap_findAux___at_Lean_Meta_SimpCongrTheorems_g LEAN_EXPORT lean_object* l_Lean_SMap_switch___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_304____spec__1(lean_object*); LEAN_EXPORT lean_object* l_Lean_SMap_toList___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__1(lean_object*); static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__6___closed__7; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__6; lean_object* l_Lean_getAttrParamOptPrio(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_ConstantInfo_levelParams(lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____closed__10; static lean_object* l_repr___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__14___closed__3; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__8; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__5; LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpCongrTheorem_onlyMVarsAt___lambda__1___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__3(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____closed__6; @@ -143,34 +144,33 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tact lean_object* lean_array_fget(lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____closed__5; LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148_(lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__4; lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallMetaTelescopeReducingAux(lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlMAux___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__5(lean_object*); lean_object* lean_st_ref_take(lean_object*, lean_object*); lean_object* l_Lean_ScopedEnvExtension_addLocalEntry___rarg(lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__6; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__7; lean_object* lean_nat_sub(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Meta_SimpCongrTheorems_lemmas___default___spec__1(lean_object*); lean_object* l_Std_RBNode_insert___at_Lean_Level_collectMVars___spec__1(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__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_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_304____closed__4; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__7; LEAN_EXPORT lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Meta_SimpCongrTheorems_get___spec__5(lean_object*, lean_object*); static lean_object* l_repr___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__14___closed__2; static size_t l_Std_PersistentHashMap_findAux___at_Lean_Meta_SimpCongrTheorems_get___spec__3___closed__1; LEAN_EXPORT lean_object* l_Std_Format_joinSep___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__17(lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkSimpCongrTheorem___closed__4; LEAN_EXPORT lean_object* l_Lean_Meta_addSimpCongrTheoremEntry(lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__2; lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkSimpCongrTheorem___closed__2; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__3; lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*); lean_object* l_Std_mkHashMapImp___rarg(lean_object*); static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpCongrTheorem___spec__1___closed__7; static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__5___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_getSimpCongrTheorems___boxed(lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__3; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___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_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__5; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__19; uint64_t l_Lean_Name_hash(lean_object*); lean_object* l_Nat_repr(lean_object*); @@ -194,17 +194,21 @@ LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at_Lean_Meta_mkSimpCongrTheore LEAN_EXPORT lean_object* l_Lean_Meta_instReprSimpCongrTheorems; LEAN_EXPORT lean_object* l_Lean_Meta_getSimpCongrTheorems___rarg___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__10(lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__1; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__5; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__6; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); size_t lean_usize_shift_left(size_t, size_t); static lean_object* l_Lean_Meta_instInhabitedSimpCongrTheorem___closed__2; lean_object* lean_array_to_list(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed(lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__14; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__28; LEAN_EXPORT lean_object* l_Lean_Meta_SimpCongrTheorems_lemmas___default; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__25; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__5; LEAN_EXPORT lean_object* l_repr___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__14(lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__10; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____closed__3; uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_304____closed__2; @@ -228,7 +232,6 @@ LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Meta_SimpCo size_t lean_usize_mul(size_t, size_t); LEAN_EXPORT uint8_t l_Lean_Meta_mkSimpCongrTheorem_onlyMVarsAt___lambda__1(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_SMap_fold___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__2(lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__7; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8(lean_object*, lean_object*, size_t, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__17; static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__3___closed__2; @@ -243,16 +246,15 @@ LEAN_EXPORT lean_object* l_Lean_Meta_instInhabitedSimpCongrTheorem; size_t lean_usize_land(size_t, size_t); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__2___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_Std_PersistentHashMap_foldlMAux___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__8___rarg(lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__6; static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__7___closed__3; static lean_object* l_Lean_Meta_SimpCongrTheorems_lemmas___default___closed__3; static lean_object* l_repr___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__14___closed__1; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__8___lambda__4(lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__6; LEAN_EXPORT lean_object* l_Std_AssocList_foldlM___at_Lean_Meta_addSimpCongrTheoremEntry___spec__10(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__7(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_304____closed__5; static lean_object* l_Lean_Expr_withAppAux___at_Lean_Meta_mkSimpCongrTheorem___spec__10___closed__1; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__10; LEAN_EXPORT lean_object* l_repr___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____spec__1(lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Meta_addSimpCongrTheoremEntry___spec__5(lean_object*, lean_object*, lean_object*, lean_object*); @@ -273,12 +275,13 @@ LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at_Lean_Meta_mkSimpCongrTheore uint8_t l_Lean_BinderInfo_isExplicit(uint8_t); LEAN_EXPORT lean_object* l_Lean_Meta_addSimpCongrTheoremEntry_insert(lean_object*, lean_object*); static lean_object* l_repr___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__14___closed__4; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__3; LEAN_EXPORT lean_object* l_Lean_Meta_addSimpCongrTheorem(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); static lean_object* l_repr___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__14___closed__8; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__3; LEAN_EXPORT lean_object* l_Lean_mkConstWithLevelParams___at_Lean_Meta_mkSimpCongrTheorem___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__1; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__7; LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpCongrTheorem_onlyMVarsAt___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_repr___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__15(lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__6___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -290,7 +293,8 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheo static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_304____closed__3; static lean_object* l_Lean_Meta_mkSimpCongrTheorem___closed__3; lean_object* lean_nat_mul(lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__1; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__1; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__2; LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlM___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__7(lean_object*); lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__26; @@ -300,18 +304,17 @@ static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__3___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_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_304_(lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727_(lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__2; +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731_(lean_object*); lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__10___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_getSimpCongrTheorems(lean_object*, lean_object*, lean_object*); lean_object* lean_mk_array(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkSimpCongrTheorem___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__4; extern lean_object* l_Lean_Expr_instBEqExpr; static lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpCongrTheorem___spec__6___closed__9; LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlMAux___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__12___rarg(lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__4; static lean_object* l_Lean_Expr_withAppAux___at_Lean_Meta_mkSimpCongrTheorem___spec__10___closed__2; lean_object* l_Lean_ScopedEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_AssocList_foldlM___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__3___rarg(lean_object*, lean_object*, lean_object*); @@ -334,8 +337,8 @@ static lean_object* l_repr___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorem static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__15; static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpCongrTheorem___spec__1___closed__4; static lean_object* l_Lean_Meta_addSimpCongrTheorem___closed__1; -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__3; +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__18; LEAN_EXPORT lean_object* l_Lean_Meta_congrExtension; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__5; @@ -354,17 +357,14 @@ lean_object* l_Lean_mkConst(lean_object*, lean_object*); lean_object* l_Lean_Expr_constName_x21(lean_object*); LEAN_EXPORT lean_object* l_Lean_SMap_fold___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__2___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_PersistentHashMap_foldlMAux___at___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____spec__12(lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__2; lean_object* lean_nat_to_int(lean_object*); lean_object* l_Std_PersistentHashMap_mkEmptyEntries(lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Meta_addSimpCongrTheoremEntry___spec__3(lean_object*, size_t, size_t, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_SMap_insert___at_Lean_Meta_addSimpCongrTheoremEntry___spec__1(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_mkConstWithLevelParams___at_Lean_Meta_mkSimpCongrTheorem___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorem____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_51____closed__11; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpCongrTheorems_0__Lean_Meta_reprSimpCongrTheorems____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_148____closed__1; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_getSimpCongrTheorems___rarg(lean_object*, lean_object*); lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); @@ -9896,7 +9896,7 @@ x_10 = l_Lean_Meta_addSimpCongrTheorem(x_1, x_9, x_3, x_4, x_5, x_6, x_7, x_8); return x_10; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__1() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__1() { _start: { uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5; @@ -9922,7 +9922,7 @@ lean_ctor_set_uint8(x_5, 13, x_4); return x_5; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__2() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -9934,7 +9934,7 @@ lean_ctor_set(x_3, 1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__3() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__3() { _start: { lean_object* x_1; lean_object* x_2; @@ -9943,23 +9943,23 @@ x_2 = lean_mk_empty_array_with_capacity(x_1); return x_2; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__4() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__4() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__3; +x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__3; x_2 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_2, 0, x_1); return x_2; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__5() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__5() { _start: { size_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = 5; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__4; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__3; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__4; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__3; x_4 = lean_unsigned_to_nat(0u); x_5 = lean_alloc_ctor(0, 4, sizeof(size_t)*1); lean_ctor_set(x_5, 0, x_2); @@ -9970,25 +9970,25 @@ lean_ctor_set_usize(x_5, 4, x_1); return x_5; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__6() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__2; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__5; +x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__2; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__5; 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_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__7() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___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; x_1 = lean_box(0); -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__1; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__6; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__1; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__6; x_4 = l_Lean_Meta_instInhabitedSimpCongrTheorem___closed__1; x_5 = lean_unsigned_to_nat(0u); x_6 = lean_alloc_ctor(0, 6, 0); @@ -10001,7 +10001,7 @@ lean_ctor_set(x_6, 5, x_1); return x_6; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__8() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -10013,12 +10013,12 @@ lean_ctor_set(x_3, 1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__9() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__9() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; x_1 = lean_unsigned_to_nat(0u); -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__8; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__8; x_3 = l_Lean_Meta_SimpCongrTheorems_lemmas___default___closed__3; x_4 = 0; x_5 = lean_alloc_ctor(0, 8, 1); @@ -10034,14 +10034,14 @@ lean_ctor_set_uint8(x_5, sizeof(void*)*8, x_4); return x_5; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__10() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__10() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = lean_box(0); -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__9; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__9; x_3 = l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpCongrTheorem___spec__1___closed__9; -x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__5; +x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__5; x_5 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_5, 0, x_2); lean_ctor_set(x_5, 1, x_3); @@ -10050,7 +10050,7 @@ lean_ctor_set(x_5, 3, x_4); return x_5; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1(lean_object* x_1, lean_object* x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1(lean_object* x_1, lean_object* x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { _start: { lean_object* x_7; lean_object* x_8; lean_object* x_9; @@ -10071,14 +10071,14 @@ x_12 = lean_st_ref_get(x_5, x_11); x_13 = lean_ctor_get(x_12, 1); lean_inc(x_13); lean_dec(x_12); -x_14 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__10; +x_14 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__10; x_15 = lean_st_mk_ref(x_14, x_13); x_16 = lean_ctor_get(x_15, 0); lean_inc(x_16); x_17 = lean_ctor_get(x_15, 1); lean_inc(x_17); lean_dec(x_15); -x_18 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__7; +x_18 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__7; lean_inc(x_5); lean_inc(x_16); x_19 = l_Lean_Meta_addSimpCongrTheorem(x_1, x_3, x_10, x_18, x_16, x_4, x_5, x_17); @@ -10170,7 +10170,7 @@ return x_37; } } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__1() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__1() { _start: { lean_object* x_1; @@ -10178,25 +10178,25 @@ x_1 = lean_mk_string_from_bytes("attribute cannot be erased", 26); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__2() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__2() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__1; +x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__1; x_2 = l_Lean_stringToMessageData(x_1); return x_2; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; lean_object* x_6; -x_5 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__2; +x_5 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__2; x_6 = l_Lean_throwError___at_Lean_AttributeImpl_erase___default___spec__1(x_5, x_2, x_3, x_4); return x_6; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__1() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__1() { _start: { lean_object* x_1; @@ -10204,17 +10204,17 @@ x_1 = lean_mk_string_from_bytes("congr", 5); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__2() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__1; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__3() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__3() { _start: { lean_object* x_1; @@ -10222,12 +10222,12 @@ x_1 = lean_mk_string_from_bytes("congruence theorem", 18); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__4() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__4() { _start: { lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; -x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__2; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__3; +x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__2; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__3; x_3 = 0; x_4 = lean_alloc_ctor(0, 2, 1); lean_ctor_set(x_4, 0, x_1); @@ -10236,29 +10236,29 @@ lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_3); return x_4; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__5() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__5() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___boxed), 6, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___boxed), 6, 0); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__6() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__6() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___boxed), 4, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___boxed), 4, 0); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__7() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__4; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__5; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__6; +x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__4; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__5; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__6; x_4 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -10266,31 +10266,31 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__7; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__7; x_3 = l_Lean_registerBuiltinAttribute(x_2, x_1); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____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_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____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) { _start: { uint8_t x_7; lean_object* x_8; x_7 = lean_unbox(x_3); lean_dec(x_3); -x_8 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1(x_1, x_2, x_7, x_4, x_5, x_6); +x_8 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1(x_1, x_2, x_7, x_4, x_5, x_6); lean_dec(x_2); return x_8; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; -x_5 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2(x_1, x_2, x_3, x_4); +x_5 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2(x_1, x_2, x_3, x_4); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); @@ -10627,45 +10627,45 @@ l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpCongrTheorem___spec__1___clo lean_mark_persistent(l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpCongrTheorem___spec__1___closed__9); l_Lean_Meta_addSimpCongrTheorem___closed__1 = _init_l_Lean_Meta_addSimpCongrTheorem___closed__1(); lean_mark_persistent(l_Lean_Meta_addSimpCongrTheorem___closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__1(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__2(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__3(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__3); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__4(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__4); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__5(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__5); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__6 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__6(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__6); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__7 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__7(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__7); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__8 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__8(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__8); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__9 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__9(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__9); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__10 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__10(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__1___closed__10); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__1(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__2(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____lambda__2___closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__1(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__2(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__3(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__3); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__4(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__4); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__5(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__5); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__6 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__6(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__6); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__7 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__7(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727____closed__7); -res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1727_(lean_io_mk_world()); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__1(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__1); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__2(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__2); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__3(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__3); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__4(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__4); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__5(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__5); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__6 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__6(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__6); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__7 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__7(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__7); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__8 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__8(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__8); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__9 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__9(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__9); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__10 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__10(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__1___closed__10); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__1(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__1); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__2(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____lambda__2___closed__2); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__1(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__1); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__2(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__2); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__3(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__3); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__4(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__4); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__5(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__5); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__6 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__6(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__6); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__7 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__7(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731____closed__7); +res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1731_(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)); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Split.c b/stage0/stdlib/Lean/Meta/Tactic/Split.c index eaf163b489..da301ffb20 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Split.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Split.c @@ -332,7 +332,7 @@ static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_Tactic_Spl LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Split_0__Lean_Meta_Split_withEqs_go___rarg___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_object*); lean_object* l_Lean_Meta_mkEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_Tactic_Split_0__Lean_Meta_Split_generalizeMatchDiscrs_mkNewTarget___spec__1___closed__9; -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Split___hyg_5633_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Split___hyg_5637_(lean_object*); LEAN_EXPORT lean_object* l_Lean_commitWhenSome_x3f___at_Lean_Meta_splitTarget_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_reduceRecMatcher_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkConst(lean_object*, lean_object*); @@ -12783,7 +12783,7 @@ x_10 = l_Lean_commitWhenSome_x3f___at_Lean_Meta_splitTarget_x3f___spec__1(x_9, x return x_10; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Split___hyg_5633_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Split___hyg_5637_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -12981,7 +12981,7 @@ l_Lean_commitWhenSome_x3f___at_Lean_Meta_splitTarget_x3f___spec__1___at_Lean_Met lean_mark_persistent(l_Lean_commitWhenSome_x3f___at_Lean_Meta_splitTarget_x3f___spec__1___at_Lean_Meta_splitTarget_x3f___spec__2___closed__1); l_Lean_Meta_splitLocalDecl_x3f___lambda__1___closed__1 = _init_l_Lean_Meta_splitLocalDecl_x3f___lambda__1___closed__1(); lean_mark_persistent(l_Lean_Meta_splitLocalDecl_x3f___lambda__1___closed__1); -res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Split___hyg_5633_(lean_io_mk_world()); +res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Split___hyg_5637_(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)); diff --git a/stage0/stdlib/Lean/Meta/UnificationHint.c b/stage0/stdlib/Lean/Meta/UnificationHint.c index 2bfd21993d..721ad1a608 100644 --- a/stage0/stdlib/Lean/Meta/UnificationHint.c +++ b/stage0/stdlib/Lean/Meta/UnificationHint.c @@ -30,7 +30,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_tryUnificationHints___lambda__1(lean_object lean_object* lean_nat_div(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_tryUnificationHints_tryCandidate___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_UnificationHint_0__Lean_Meta_decodeUnificationHint_decode___closed__1; -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_2047_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_2051_(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_81_(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_720_(lean_object*); static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_720____lambda__1___closed__8; @@ -9068,7 +9068,7 @@ lean_dec(x_3); return x_9; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_2047_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_2051_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -9348,7 +9348,7 @@ l_Lean_Meta_tryUnificationHints___lambda__2___closed__1 = _init_l_Lean_Meta_tryU lean_mark_persistent(l_Lean_Meta_tryUnificationHints___lambda__2___closed__1); l_Lean_Meta_tryUnificationHints___lambda__2___closed__2 = _init_l_Lean_Meta_tryUnificationHints___lambda__2___closed__2(); lean_mark_persistent(l_Lean_Meta_tryUnificationHints___lambda__2___closed__2); -res = l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_2047_(lean_io_mk_world()); +res = l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_2051_(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));