From 834b515592b90eb8bb0206228cf10806349c2d3e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Feb 2024 12:31:26 -0800 Subject: [PATCH] chore: update stage0 --- stage0/stdlib/Init/MetaTypes.c | 4 +- stage0/stdlib/Lean/Compiler/LCNF/Specialize.c | 158 +++--- .../Lean/Elab/PreDefinition/Structural/Eqns.c | 2 +- .../stdlib/Lean/Elab/PreDefinition/WF/Eqns.c | 2 +- stage0/stdlib/Lean/Elab/Tactic/Simp.c | 6 +- stage0/stdlib/Lean/Meta/Tactic/Acyclic.c | 2 +- stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c | 2 +- .../Lean/Meta/Tactic/Simp/SimpTheorems.c | 478 +++++++++--------- stage0/stdlib/Lean/Meta/Tactic/Simp/Types.c | 133 ++--- 9 files changed, 377 insertions(+), 410 deletions(-) diff --git a/stage0/stdlib/Init/MetaTypes.c b/stage0/stdlib/Init/MetaTypes.c index 54e4cfc2ce..3163a1ffda 100644 --- a/stage0/stdlib/Init/MetaTypes.c +++ b/stage0/stdlib/Init/MetaTypes.c @@ -490,7 +490,7 @@ static uint8_t _init_l_Lean_Meta_DSimp_Config_zetaDelta___default() { _start: { uint8_t x_1; -x_1 = 1; +x_1 = 0; return x_1; } } @@ -1098,7 +1098,7 @@ static uint8_t _init_l_Lean_Meta_Simp_Config_zetaDelta___default() { _start: { uint8_t x_1; -x_1 = 1; +x_1 = 0; return x_1; } } diff --git a/stage0/stdlib/Lean/Compiler/LCNF/Specialize.c b/stage0/stdlib/Lean/Compiler/LCNF/Specialize.c index 6c52ee2694..674f0c6ec8 100644 --- a/stage0/stdlib/Lean/Compiler/LCNF/Specialize.c +++ b/stage0/stdlib/Lean/Compiler/LCNF/Specialize.c @@ -18,6 +18,7 @@ lean_object* l_Lean_Compiler_LCNF_LetDecl_updateValue(lean_object*, lean_object* lean_object* l_Lean_Compiler_LCNF_Specialize_findSpecCache_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__4; static lean_object* l_Lean_addTrace___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__5___closed__2; +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__8; static lean_object* l_Lean_Compiler_LCNF_allFVarM___at_Lean_Compiler_LCNF_Specialize_isGround___spec__1___rarg___closed__1; lean_object* lean_mk_empty_array_with_capacity(lean_object*); lean_object* l_Lean_Compiler_LCNF_LetValue_forFVarM___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__3(lean_object*, lean_object*); @@ -31,11 +32,11 @@ lean_object* l_Lean_Compiler_LCNF_Specialize_isGround___rarg___lambda__1___boxed static lean_object* l_Lean_Compiler_LCNF_Specialize_instMonadScopeSpecializeM___closed__2; LEAN_EXPORT lean_object* l_Lean_addTrace___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_cacheSpec(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__4; lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Simp_withDiscrCtorImp_updateCtx___spec__5(size_t, size_t, lean_object*); LEAN_EXPORT lean_object* l_Lean_isTracingEnabledFor___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__11; lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__6(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_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__1; static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__14; lean_object* l_Lean_Compiler_LCNF_Code_inferType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Specialize_expandCodeDecls___spec__2___boxed(lean_object*, lean_object*, lean_object*); @@ -51,7 +52,6 @@ static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Specialize_expandCodeDecls___spec__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_shouldSpecialize(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_usize_dec_eq(size_t, size_t); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__15; lean_object* l_Lean_Compiler_LCNF_Specialize_Collector_collect___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Decl_saveBase(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Decl_etaExpand(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -59,7 +59,6 @@ static lean_object* l_panic___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f lean_object* l_Lean_Compiler_LCNF_Specialize_visitCode___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_isGround___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_instInhabitedReaderT___rarg___boxed(lean_object*, lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__9; lean_object* l_Lean_Expr_bvar___override(lean_object*); lean_object* lean_array_fget(lean_object*, lean_object*); lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*); @@ -67,7 +66,6 @@ static lean_object* l_Lean_Compiler_LCNF_Specialize_visitCode___closed__1; static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__6; static lean_object* l_Lean_Compiler_LCNF_Expr_forFVarM___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__5___closed__3; lean_object* l_ReaderT_instMonadReaderT___rarg(lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__2; lean_object* l_Lean_Compiler_LCNF_Specialize_isGround___at_Lean_Compiler_LCNF_Specialize_shouldSpecialize___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_updateFunDeclImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__5___closed__4; @@ -84,7 +82,7 @@ lean_object* l_Lean_Name_mkStr5(lean_object*, lean_object*, lean_object*, lean_o lean_object* l_ReaderT_bind___at_Lean_Compiler_LCNF_FunDeclCore_toExprM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_stringToMessageData(lean_object*); uint8_t l___private_Lean_Util_Trace_0__Lean_checkTraceOption(lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__3; +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__6; lean_object* l_Lean_Compiler_LCNF_allFVarM___at_Lean_Compiler_LCNF_Specialize_shouldSpecialize___spec__2___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_shouldSpecialize___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -95,7 +93,9 @@ lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext(lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____spec__3(lean_object*, size_t, size_t, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_Array_BasicAux_0__mapMonoMImp_go___at_Lean_Compiler_LCNF_Specialize_visitCode___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__5___closed__2; +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__9; lean_object* l_List_mapTR_loop___at_Lean_mkConstWithLevelParams___spec__1(lean_object*, lean_object*); +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__7; lean_object* l_Lean_Compiler_LCNF_mkForallParams(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_instInhabitedPUnit; static lean_object* l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____lambda__1___closed__5; @@ -105,6 +105,7 @@ size_t lean_ptr_addr(lean_object*); lean_object* l_Lean_Name_mkStr3(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___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*); size_t lean_usize_of_nat(lean_object*); +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__10; LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_Compiler_LCNF_Specialize_Collector_collect___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____closed__8; lean_object* l_Lean_Compiler_LCNF_eraseDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -115,13 +116,11 @@ static lean_object* l_Lean_Compiler_LCNF_Specialize_mkSpecDecl___closed__2; lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___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* l_Lean_Compiler_LCNF_Specialize_shouldSpecialize___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_specCacheExt; -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__10; lean_object* lean_st_ref_take(lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Decl_internalize(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_ToExpr_abstractM___boxed(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_specialize___closed__1; lean_object* l_Lean_Compiler_LCNF_Expr_forFVarM___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__5(lean_object*, lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__13; lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normArgImp(lean_object*, lean_object*, uint8_t); lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Internalize_internalizeFunDecl___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -141,6 +140,7 @@ lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_ob LEAN_EXPORT uint8_t l_Lean_HashMapImp_contains___at_Lean_Compiler_LCNF_Specialize_Collector_collect___spec__1(lean_object*, lean_object*); lean_object* l_Lean_registerTraceClass(lean_object*, uint8_t, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____lambda__1___closed__4; +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__12; lean_object* l_Lean_RBNode_findCore___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__2(lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_specialize___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_specialize___closed__3; @@ -160,6 +160,7 @@ static lean_object* l_Lean_Compiler_LCNF_Specialize_cacheSpec___closed__3; lean_object* l_Lean_Compiler_LCNF_Specialize_addEntry(lean_object*, lean_object*); uint64_t l___private_Lean_Expr_0__Lean_hashFVarId____x40_Lean_Expr___hyg_1674_(lean_object*); lean_object* lean_st_mk_ref(lean_object*, lean_object*); +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__13; lean_object* lean_array_to_list(lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_mkSpecDecl___closed__4; lean_object* l_Lean_Compiler_LCNF_normLevelParams(lean_object*); @@ -179,6 +180,7 @@ static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__ lean_object* l_Lean_Compiler_LCNF_Closure_collectArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_isTracingEnabledFor___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_addTrace___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__14; lean_object* l_Lean_Compiler_LCNF_Specialize_findSpecCache_x3f(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_HashMapImp_contains___at_Lean_Compiler_LCNF_Specialize_Collector_collect___spec__1___boxed(lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____closed__2; @@ -212,11 +214,11 @@ static lean_object* l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_ lean_object* l_Lean_Compiler_LCNF_Specialize_visitCode(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_SMap_switch___at_Lean_Compiler_SpecState_switch___spec__2(lean_object*); static lean_object* l_Lean_Compiler_LCNF_Expr_forFVarM___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__5___closed__2; +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__3; lean_object* l_Lean_Compiler_LCNF_Specialize_mkKey(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__5___closed__1; size_t lean_hashmap_mk_idx(lean_object*, uint64_t); lean_object* l_Array_append___rarg(lean_object*, lean_object*); -lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238_(lean_object*); LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___spec__2(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Compiler_LCNF_instMonadCompilerM; extern lean_object* l_Lean_inheritedTraceOptions; @@ -224,15 +226,15 @@ lean_object* l_Lean_Compiler_LCNF_Specialize_Collector_collect___lambda__1___box lean_object* l_Lean_MessageData_ofExpr(lean_object*); lean_object* l_Lean_Compiler_LCNF_getSpecParamInfoCore_x3f(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__7(lean_object*, lean_object*, size_t, size_t, lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__12; lean_object* l_Lean_Compiler_LCNF_Specialize_isGround___at_Lean_Compiler_LCNF_Specialize_shouldSpecialize___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__11; lean_object* l_Lean_Compiler_LCNF_attachCodeDecls(lean_object*, lean_object*); lean_object* l_Lean_Meta_isInstance(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___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_object*, lean_object*); static lean_object* l_Lean_addTrace___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__5___closed__3; lean_object* lean_name_append_index_after(lean_object*, lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__14; lean_object* l_Lean_Compiler_LCNF_Specialize_expandCodeDecls___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__15; LEAN_EXPORT lean_object* l___private_Init_Data_Array_BasicAux_0__mapMonoMImp___at_Lean_Compiler_LCNF_Specialize_visitCode___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_allFVarM___at_Lean_Compiler_LCNF_Specialize_isGround___spec__1(lean_object*); LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -242,20 +244,18 @@ static lean_object* l_Lean_Compiler_LCNF_Specialize_cacheSpec___closed__1; LEAN_EXPORT lean_object* l_panic___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__6(lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_getRemainingArgs___spec__1(lean_object*, size_t, size_t, lean_object*); lean_object* l_Lean_Compiler_LCNF_allFVarM___at_Lean_Compiler_LCNF_Specialize_isGround___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229_(lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____spec__2(lean_object*, size_t, size_t, lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__6; lean_object* l_Lean_HashMap_insert___at_Lean_Compiler_LCNF_addFVarSubst___spec__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_expandCodeDecls_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Decl_simp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_Collector_collect___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__11; lean_object* l_Lean_RBTree_contains___rarg___boxed(lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go___spec__2(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_Collector_collect(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_Compiler_LCNF_Specialize_instMonadScopeSpecializeM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__7; lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_allFVarM___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__2___boxed(lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_getRemainingArgs(lean_object*, lean_object*); @@ -279,14 +279,12 @@ lean_object* l_Array_ofSubarray___rarg(lean_object*); lean_object* l_Lean_RBNode_insert___at_Lean_FVarIdSet_insert___spec__1(lean_object*, lean_object*, lean_object*); lean_object* l_OptionT_instMonadOptionT___rarg(lean_object*); lean_object* lean_erase_macro_scopes(lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__8; lean_object* lean_expr_instantiate_rev(lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_instMonadScopeSpecializeM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Decl_instantiateValueLevelParams(lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46_(lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go(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_mkHashMapImp___rarg(lean_object*); -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__1; static lean_object* l_Lean_Compiler_LCNF_Specialize_instInhabitedCacheEntry___closed__1; lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___boxed(lean_object**); lean_object* l___private_Lean_Compiler_LCNF_Basic_0__Lean_Compiler_LCNF_updateAltCodeImp(lean_object*, lean_object*); @@ -306,6 +304,7 @@ lean_object* l_Lean_Compiler_LCNF_Specialize_getRemainingArgs___boxed(lean_objec uint8_t l_Lean_Compiler_LCNF_Specialize_Collector_collect___lambda__1(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Expr_forFVarM___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__5___closed__4; lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__4; lean_object* l_Lean_Expr_instantiateLevelParamsNoCache(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_ToExpr_withParams_go___at_Lean_Compiler_LCNF_Specialize_mkKey___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_filterMapM___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__3___boxed(lean_object*, lean_object*, lean_object*); @@ -330,7 +329,6 @@ lean_object* l_Lean_Compiler_LCNF_FunDeclCore_toExpr(lean_object*, lean_object*) uint8_t l_Lean_Compiler_LCNF_allFVarM___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__2(lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__13; lean_object* l_Lean_Compiler_LCNF_Specialize_mkSpecDecl(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_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__5; lean_object* l_Lean_Compiler_LCNF_getSpecParamInfo_x3f___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_Collector_collect___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -340,12 +338,14 @@ lean_object* lean_array_uset(lean_object*, size_t, lean_object*); lean_object* l_Lean_MessageData_ofName(lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_mkSpecDecl___closed__1; static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__3; +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__5; LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Specialize_withLetDecl___spec__8(lean_object*, lean_object*, size_t, size_t, lean_object*); static lean_object* l_panic___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__6___closed__1; lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Specialize_expandCodeDecls___spec__1(size_t, size_t, lean_object*); lean_object* lean_expr_abstract_range(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_Collector_collect___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__2; LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_specialize; static lean_object* l_Lean_Compiler_LCNF_Specialize_Collector_collect___closed__2; LEAN_EXPORT lean_object* l_panic___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -10207,7 +10207,7 @@ lean_dec(x_1); return x_12; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__1() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -10217,7 +10217,7 @@ x_3 = l_Lean_Name_mkStr2(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__2() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -10227,27 +10227,27 @@ x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__3() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__2; +x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__2; x_2 = l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____closed__2; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__4() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__3; +x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__3; x_2 = l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____closed__3; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__5() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__5() { _start: { lean_object* x_1; @@ -10255,17 +10255,17 @@ x_1 = lean_mk_string_from_bytes("initFn", 6); return x_1; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__6() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__4; -x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__5; +x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__4; +x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__5; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__7() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__7() { _start: { lean_object* x_1; @@ -10273,57 +10273,57 @@ x_1 = lean_mk_string_from_bytes("_@", 2); return x_1; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__8() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__6; -x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__7; +x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__6; +x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__7; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__9() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__9() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__8; +x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__8; x_2 = l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____closed__1; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__10() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__10() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__9; +x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__9; x_2 = l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____closed__2; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__11() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__11() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__10; +x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__10; x_2 = l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____closed__3; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__12() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__12() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__11; +x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__11; x_2 = l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_46____closed__4; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__13() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__13() { _start: { lean_object* x_1; @@ -10331,33 +10331,33 @@ x_1 = lean_mk_string_from_bytes("_hyg", 4); return x_1; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__14() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__14() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__12; -x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__13; +x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__12; +x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__13; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__15() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__15() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__14; -x_2 = lean_unsigned_to_nat(4238u); +x_1 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__14; +x_2 = lean_unsigned_to_nat(4229u); x_3 = l_Lean_Name_num___override(x_1, x_2); return x_3; } } -lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238_(lean_object* x_1) { +lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229_(lean_object* x_1) { _start: { lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; -x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__1; +x_2 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__1; x_3 = 1; -x_4 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__15; +x_4 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__15; x_5 = l_Lean_registerTraceClass(x_2, x_3, x_4, x_1); if (lean_obj_tag(x_5) == 0) { @@ -10647,37 +10647,37 @@ l_Lean_Compiler_LCNF_specialize___closed__3 = _init_l_Lean_Compiler_LCNF_special lean_mark_persistent(l_Lean_Compiler_LCNF_specialize___closed__3); l_Lean_Compiler_LCNF_specialize = _init_l_Lean_Compiler_LCNF_specialize(); lean_mark_persistent(l_Lean_Compiler_LCNF_specialize); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__1 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__1(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__1); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__2 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__2(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__2); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__3 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__3(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__3); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__4 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__4(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__4); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__5 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__5(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__5); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__6 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__6(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__6); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__7 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__7(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__7); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__8 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__8(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__8); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__9 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__9(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__9); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__10 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__10(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__10); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__11 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__11(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__11); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__12 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__12(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__12); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__13 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__13(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__13); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__14 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__14(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__14); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__15 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__15(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238____closed__15); -if (builtin) {res = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4238_(lean_io_mk_world()); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__1 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__1(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__1); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__2 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__2(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__2); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__3 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__3(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__3); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__4 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__4(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__4); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__5 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__5(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__5); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__6 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__6(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__6); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__7 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__7(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__7); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__8 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__8(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__8); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__9 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__9(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__9); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__10 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__10(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__10); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__11 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__11(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__11); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__12 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__12(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__12); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__13 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__13(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__13); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__14 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__14(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__14); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__15 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__15(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229____closed__15); +if (builtin) {res = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4229_(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/Eqns.c b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c index d09c1efcc2..abd5937859 100644 --- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c +++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c @@ -382,7 +382,7 @@ lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 12, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 13, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 14, x_3); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 15, x_3); -lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_4); +lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_3); return x_6; } } diff --git a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c index 7b7115c387..e60b54224d 100644 --- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c +++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c @@ -3515,7 +3515,7 @@ lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 12, x_3); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 13, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 14, x_3); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 15, x_3); -lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_4); +lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_3); return x_6; } } diff --git a/stage0/stdlib/Lean/Elab/Tactic/Simp.c b/stage0/stdlib/Lean/Elab/Tactic/Simp.c index f3bb3d618e..1c1b4d058a 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/Simp.c +++ b/stage0/stdlib/Lean/Elab/Tactic/Simp.c @@ -3149,7 +3149,7 @@ lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 12, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 13, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 14, x_3); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 15, x_3); -lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_4); +lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_3); return x_6; } } @@ -3446,7 +3446,7 @@ lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 12, x_3); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 13, x_3); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 14, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 15, x_4); -lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_3); +lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_4); return x_6; } } @@ -3638,7 +3638,7 @@ lean_ctor_set_uint8(x_4, 6, x_3); lean_ctor_set_uint8(x_4, 7, x_3); lean_ctor_set_uint8(x_4, 8, x_1); lean_ctor_set_uint8(x_4, 9, x_3); -lean_ctor_set_uint8(x_4, 10, x_1); +lean_ctor_set_uint8(x_4, 10, x_3); return x_4; } } diff --git a/stage0/stdlib/Lean/Meta/Tactic/Acyclic.c b/stage0/stdlib/Lean/Meta/Tactic/Acyclic.c index fd6f51e57d..9ba771d8e4 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Acyclic.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Acyclic.c @@ -405,7 +405,7 @@ lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 12, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 13, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 14, x_3); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 15, x_3); -lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_4); +lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_3); return x_6; } } diff --git a/stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c b/stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c index 5031746f3a..8c42b3dcd6 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c @@ -19130,7 +19130,7 @@ lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 12, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 13, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 14, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 15, x_3); -lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_4); +lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_3); return x_6; } } diff --git a/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c b/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c index 2e43141d50..5ec3f21f48 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c @@ -15,23 +15,23 @@ extern "C" { #endif lean_object* l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_createNodes___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_checkTypeIsProp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__3; lean_object* l_Lean_Expr_const___override(lean_object*, lean_object*); static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__11; LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheoremsArray_isDeclToUnfold___boxed(lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__2; static lean_object* l_Lean_Meta_SimpTheorem_keys___default___closed__1; static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__12; lean_object* l___private_Init_Util_0__outOfBounds___rarg(lean_object*); lean_object* l_Lean_Name_reprPrec(lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__4; LEAN_EXPORT lean_object* l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_insertVal_loop___at_Lean_Meta_addSimpTheoremEntry___spec__10(lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__5; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____closed__13; LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpExt(lean_object*, lean_object*); static lean_object* l_Lean_Meta_isRflProofCore___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_isRflProofCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_getAttrParamOptPrio(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_erase___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorem_getValue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_isDeclToUnfold___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_insertAux___at_Lean_Meta_addSimpTheoremEntry___spec__9(lean_object*, lean_object*, lean_object*, lean_object*); @@ -59,14 +59,11 @@ static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_ static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__9; LEAN_EXPORT uint8_t l_Lean_PersistentHashMap_containsAtAux___at_Lean_Meta_SimpTheorems_erase___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Lean_Meta_SimpTheoremsArray_isErased(lean_object*, lean_object*); -LEAN_EXPORT lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917_; LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__3___closed__2; static lean_object* l_panic___at_Lean_Meta_addSimpTheoremEntry___spec__13___closed__1; static lean_object* l_panic___at___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___spec__2___closed__1; -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__8; lean_object* l_Lean_ConstantInfo_type(lean_object*); -LEAN_EXPORT lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5449_; LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpAttr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_registerDeclToUnfoldThms(lean_object*, lean_object*, lean_object*); @@ -80,6 +77,7 @@ LEAN_EXPORT lean_object* l_Lean_HashMap_insert___at_Lean_Meta_registerSimpAttr__ static lean_object* l_Lean_Meta_mkSimpExt___closed__3; static lean_object* l_Lean_Meta_isRflProofCore___closed__1; lean_object* l_Lean_Meta_mkEqSymm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__4; lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____closed__2; @@ -87,7 +85,6 @@ static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_ LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_isLemma___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_SimpTheoremsArray_isLetDeclToUnfold___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); size_t lean_uint64_to_usize(uint64_t); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__15; static lean_object* l_Lean_Meta_SimpTheorem_getValue___closed__3; uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -107,6 +104,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_pre___default; LEAN_EXPORT lean_object* l_panic___at___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__11; lean_object* l_Lean_instBEqLocalInstance___boxed(lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__17; static lean_object* l_Lean_Meta_instToFormatSimpTheorem___closed__3; size_t lean_usize_mul(size_t, size_t); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_addConst___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -123,7 +121,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_ lean_object* l_Lean_Expr_proj___override(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_bvar___override(lean_object*); lean_object* lean_array_fget(lean_object*, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__5; lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__3___closed__4; LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Meta_addSimpTheoremEntry_updateLemmaNames___spec__4(lean_object*, lean_object*, lean_object*, lean_object*); @@ -132,20 +129,21 @@ static lean_object* l_Lean_Meta_instInhabitedOrigin___closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_addSimpTheoremEntry_updateLemmaNames(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_AssocList_contains___at_Lean_Meta_registerSimpAttr___spec__2___boxed(lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1; static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__13; LEAN_EXPORT lean_object* l___private_Init_Data_Array_BinSearch_0__Array_binInsertAux___at_Lean_Meta_addSimpTheoremEntry___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__9; LEAN_EXPORT lean_object* l_Lean_Meta_instBEqSimpTheorem___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5537____spec__1___boxed(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*); LEAN_EXPORT lean_object* l_Lean_Meta_ppOrigin___rarg___lambda__1(uint8_t, uint8_t, lean_object*, lean_object*); static lean_object* l_Lean_Meta_instInhabitedSimpTheorem___closed__1; uint8_t l_Lean_ConstantInfo_hasValue(lean_object*); LEAN_EXPORT lean_object* l_List_mapM_loop___at___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__19; static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__13; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__3; -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5537_(lean_object*); LEAN_EXPORT uint64_t l_Lean_Meta_instHashableOrigin(lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__5; lean_object* l_Lean_stringToMessageData(lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_SimpTheoremsArray_eraseTheorem___spec__1(lean_object*, size_t, size_t, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -158,14 +156,18 @@ LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_toUnfoldThms___default; LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_shouldPreprocess___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Lean_Meta_SimpTheorems_isLemma(lean_object*, lean_object*); static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__8; +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__5; +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__16; extern lean_object* l_Lean_Expr_instBEqExpr; lean_object* l_Lean_throwError___at_Lean_Meta_setInlineAttribute___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__13; lean_object* l_Lean_ScopedEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Lean_Meta_instBEqOrigin(lean_object*, lean_object*); lean_object* l_instBEqProd___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__18; LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpAttr___lambda__2(lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699_(lean_object*); lean_object* l_Lean_Expr_appArg_x21(lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__4; LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_empty___at_Lean_Meta_SimpTheorems_lemmaNames___default___spec__1; lean_object* l_List_mapTR_loop___at_Lean_mkConstWithLevelParams___spec__1(lean_object*, lean_object*); static lean_object* l_Lean_Meta_isRflProofCore___closed__3; @@ -173,10 +175,10 @@ LEAN_EXPORT lean_object* l_Lean_Meta_ppSimpTheorem___rarg___lambda__1(lean_objec LEAN_EXPORT lean_object* l_Lean_Meta_getSEvalTheorems___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_AssocList_replace___at_Lean_Meta_registerSimpAttr___spec__6(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__5; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__4; LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_addDeclToUnfold___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____closed__15; lean_object* l_instHashableArray___rarg___boxed(lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__6; lean_object* l_Lean_Name_mkStr3(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkSimpExt___closed__1; lean_object* l_Lean_Meta_mkAuxLemma(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -190,6 +192,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_add(lean_object*, lean_object* static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____closed__6; LEAN_EXPORT lean_object* l_Lean_Meta_ppOrigin___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__14; +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700_(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorem_getValue___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_addSimpTheoremEntry(lean_object*, lean_object*); static lean_object* l_Lean_Meta_isRflProofCore___closed__8; @@ -197,10 +200,8 @@ LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_erase(lean_object*); static lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheoremEntry___spec__1___closed__4; static lean_object* l_Lean_Meta_SimpTheorems_erase___rarg___closed__2; lean_object* l_Lean_ScopedEnvExtension_addScopedEntry___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__9; lean_object* lean_st_ref_take(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLetDeclImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__6; LEAN_EXPORT lean_object* l_Lean_Meta_sevalSimpExtension; lean_object* l_Lean_getConstInfo___at___private_Lean_Compiler_InlineAttrs_0__Lean_Compiler_isValidMacroInline___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_add___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*); @@ -211,11 +212,10 @@ static lean_object* l_Lean_Meta_ppOrigin___rarg___lambda__1___closed__1; static lean_object* l_Lean_PersistentHashMap_insertAux___at_Lean_Meta_addSimpTheoremEntry_updateLemmaNames___spec__2___closed__3; uint8_t lean_expr_eqv(lean_object*, lean_object*); static lean_object* l_Lean_Meta_instToFormatSimpTheorem___closed__4; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__1; +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__15; lean_object* l_Lean_registerSimpleScopedEnvExtension___rarg(lean_object*, lean_object*); static lean_object* l_Lean_Meta_getSimpTheorems___closed__1; static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__2; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__3; static lean_object* l_Lean_Meta_SimpTheorems_erase___rarg___closed__1; lean_object* lean_nat_to_int(lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____closed__12; @@ -225,10 +225,8 @@ LEAN_EXPORT lean_object* l_Lean_Meta_addSimpTheorem___boxed(lean_object*, lean_o lean_object* lean_nat_div(lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__1___closed__1; 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*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__1; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____closed__10; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_mkSimpTheorems___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*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__13; LEAN_EXPORT lean_object* l_Lean_Meta_Origin_key___boxed(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Lean_Meta_SimpTheorems_isLetDeclToUnfold(lean_object*, lean_object*); @@ -245,7 +243,6 @@ LEAN_EXPORT uint8_t l_Lean_Meta_SimpTheoremsArray_isDeclToUnfold(lean_object*, l lean_object* l_Lean_Syntax_getKind(lean_object*); static lean_object* l_Lean_Meta_instToFormatSimpTheorem___closed__1; static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__3; -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__22; static lean_object* l_Lean_Meta_SimpTheorem_getValue___closed__4; static lean_object* l_Lean_Meta_SimpTheorems_pre___default___closed__1; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_addSimpTheorem___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -272,17 +269,17 @@ LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_SimpTheoremsArray_isDe lean_object* lean_st_mk_ref(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_ppSimpTheorem___rarg___lambda__2(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_getSEvalTheorems___closed__1; -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__11; LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_addDeclToUnfoldCore(lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_checkTypeIsProp___closed__1; lean_object* l_Lean_Meta_mkEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__17; static lean_object* l_Lean_PersistentHashMap_empty___at_Lean_Meta_SimpTheorems_lemmaNames___default___spec__1___closed__5; lean_object* l_Lean_ScopedEnvExtension_modifyState___rarg(lean_object*, lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__21; LEAN_EXPORT uint8_t l_Lean_Meta_SimpTheorem_post___default; LEAN_EXPORT lean_object* l_Lean_Meta_ppSimpTheorem___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_registerSimpAttr___closed__1; uint8_t l_Lean_Meta_DiscrTree_Key_lt(lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__11; extern lean_object* l_Lean_Expr_instHashableExpr; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_SimpTheorems_addDeclToUnfold___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Lean_Meta_SimpTheorem_perm___default; @@ -294,7 +291,6 @@ static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_ LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpAttr___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_post___default; LEAN_EXPORT lean_object* l_Array_indexOfAux___at_Lean_Meta_SimpTheorems_eraseCore___spec__3___boxed(lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__25; static lean_object* l_Lean_Meta_instReprOrigin___closed__1; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___closed__1; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpAttr___spec__2(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -302,6 +298,7 @@ static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_ lean_object* l_panic___at_Lean_Expr_appFn_x21___spec__1(lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___closed__2; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____closed__3; +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__3; static lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheoremEntry___spec__1___closed__3; static lean_object* l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_insertAux___at_Lean_Meta_addSimpTheoremEntry___spec__9___closed__1; lean_object* l_Lean_instHashableLocalInstance___boxed(lean_object*); @@ -319,12 +316,14 @@ lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__3___closed__5; lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_binInsertM___at_Lean_Meta_addSimpTheoremEntry___spec__11(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_isRflTheorem(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_mkSimpTheorems___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_erase___at_Lean_Meta_mkSimpAttr___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_SimpTheorems_erase___rarg___closed__3; lean_object* l_Lean_PersistentHashMap_find_x3f___at_Lean_Meta_getEqnsFor_x3f___spec__1(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocessProof(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__1; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_SimpTheorems_addDeclToUnfold___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_appFn_x21(lean_object*); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_erase___at_Lean_Meta_SimpTheorems_eraseCore___spec__1___boxed(lean_object*, lean_object*); @@ -333,13 +332,13 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_SimpTheoremsArray LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_checkBadRewrite(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__1___closed__3; static lean_object* l_Lean_Meta_SimpTheorems_addDeclToUnfold___closed__1; -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__10; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__3; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__4; LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_registerSimpAttr(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheoremEntry___spec__1___closed__1; static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__16; +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__10; lean_object* l_Lean_Meta_DiscrTree_mkPath(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_usize_to_nat(size_t); size_t lean_hashmap_mk_idx(lean_object*, uint64_t); @@ -347,39 +346,39 @@ lean_object* l_Lean_Meta_withNewMCtxDepth___at___private_Lean_Meta_WHNF_0__Lean_ lean_object* l_Lean_Meta_instInhabitedMetaM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_instBEqOrigin___boxed(lean_object*, lean_object*); static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__12; -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__3; +LEAN_EXPORT lean_object* l_Lean_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5538____spec__1___boxed(lean_object*); static lean_object* l_Lean_Meta_instInhabitedSimpTheorems___closed__2; LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5538_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674_(lean_object*); LEAN_EXPORT lean_object* l_Lean_HashMapImp_expand___at_Lean_Meta_registerSimpAttr___spec__3(lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__23; lean_object* l_Lean_MessageData_ofExpr(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__6(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_containsAux___at_Lean_Meta_SimpTheorems_erase___spec__2___boxed(lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__16; LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_checkBadRewrite___closed__1; static lean_object* l_Lean_Meta_SimpTheorem_getValue___closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_SimpExtension_getTheorems(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT 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___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__18; static lean_object* l_Lean_Meta_isRflProofCore___closed__6; LEAN_EXPORT lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_mkSimpAttr___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpAttr___lambda__2___boxed(lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__21; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__3___closed__6; LEAN_EXPORT uint8_t l_Lean_AssocList_contains___at_Lean_Meta_registerSimpAttr___spec__2(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at_Lean_Meta_addSimpTheoremEntry___spec__3(lean_object*, size_t, lean_object*); LEAN_EXPORT uint8_t l_Lean_PersistentHashMap_containsAux___at_Lean_Meta_SimpTheorems_isLemma___spec__2(lean_object*, size_t, lean_object*); static lean_object* l_Lean_Meta_ppSimpTheorem___rarg___lambda__1___closed__1; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__3___closed__10; -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__26; LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_shouldPreprocess(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__2___closed__1; LEAN_EXPORT lean_object* l_List_forIn_loop___at___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremsFromConst___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__14; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___lambda__2___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorem_priority___default; lean_object* l___private_Init_Meta_0__Lean_Syntax_reprSyntax____x40_Init_Meta___hyg_2056_(lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__22; static lean_object* l_Lean_Meta_ppOrigin___rarg___lambda__1___closed__4; +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__25; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__5; LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at_Lean_Meta_addSimpTheoremEntry___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_ppOrigin___rarg___lambda__1___closed__2; @@ -396,8 +395,8 @@ static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_ static lean_object* l_Lean_Meta_SimpTheorems_erase___rarg___closed__4; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__3___closed__9; static size_t l_Lean_PersistentHashMap_insertAux___at_Lean_Meta_addSimpTheoremEntry_updateLemmaNames___spec__2___closed__2; -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673_(lean_object*); static lean_object* l_Lean_Meta_isRflProofCore___closed__4; +LEAN_EXPORT lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918_; LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_addLetDeclToUnfold(lean_object*, lean_object*); static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__2; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____closed__1; @@ -406,21 +405,23 @@ LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_erase___at_Lean_Meta_mkSimpAtt uint8_t lean_nat_dec_lt(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheoremsArray_isLetDeclToUnfold___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__6___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___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__20; lean_object* l_Lean_instantiateMVars___at___private_Lean_Meta_Basic_0__Lean_Meta_isClassApp_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___closed__3; static lean_object* l_Lean_Meta_ppOrigin___rarg___lambda__1___closed__3; LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_containsAtAux___at_Lean_Meta_SimpTheorems_erase___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_ppOrigin___rarg___lambda__1___closed__6; LEAN_EXPORT lean_object* l_Lean_Meta_mkSimpTheorems___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___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__26; lean_object* l_id___rarg___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux_traverse___at_Lean_Meta_addSimpTheoremEntry___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_DiscrTree_instInhabitedDiscrTree(lean_object*); lean_object* l_Lean_Name_mkStr2(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_instInhabitedSimpTheorems; -LEAN_EXPORT lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5573_; lean_object* l_Lean_indentExpr(lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__4; +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__24; lean_object* l_Lean_PersistentHashMap_mkEmptyEntries(lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__2; LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_SimpTheoremsArray_isLetDeclToUnfold___spec__1(lean_object*, lean_object*, size_t, size_t); static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__6; LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_SimpTheoremsArray_isErased___spec__1(lean_object*, lean_object*, size_t, size_t); @@ -430,10 +431,9 @@ LEAN_EXPORT lean_object* l_Lean_Meta_getSimpExtension_x3f(lean_object*, lean_obj LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Expr_isConstOf(lean_object*, 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*); -LEAN_EXPORT lean_object* l_Lean_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5537____spec__1(lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__6; lean_object* lean_array_set(lean_object*, lean_object*, lean_object*); uint64_t l_Lean_Name_hash___override(lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__6; LEAN_EXPORT lean_object* l_Array_indexOfAux___at_Lean_Meta_SimpTheorems_eraseCore___spec__3(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_insertAux___at_Lean_Meta_addSimpTheoremEntry___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_erase___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*); @@ -446,9 +446,9 @@ static lean_object* l_Lean_Meta_mkSimpAttr___lambda__1___closed__10; static lean_object* l_Lean_PersistentHashMap_empty___at_Lean_Meta_SimpTheorems_lemmaNames___default___spec__1___closed__3; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_mkSimpAttr___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Repr_addAppParen(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5450_; uint8_t l_Lean_Syntax_isNone(lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____closed__14; -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__2; static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__3; lean_object* lean_panic_fn(lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_reprOrigin____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_79____closed__16; @@ -457,31 +457,30 @@ LEAN_EXPORT lean_object* l_Lean_Meta_withLetDecl___at___private_Lean_Meta_Tactic static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__7; lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* l_Lean_ScopedEnvExtension_getState___rarg(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5574_; LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_erase___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_insertAt_x21___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_getAppFn(lean_object*); static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__5; LEAN_EXPORT lean_object* l_Array_binInsertM___at_Lean_Meta_addSimpTheoremEntry___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_mkSimpTheoremCore___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_SimpTheorems___hyg_5674____closed__3; lean_object* lean_nat_mul(lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__2___closed__3; lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_ppOrigin(lean_object*); static lean_object* l_Lean_Meta_instToFormatSimpTheorem___closed__2; lean_object* l_Lean_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_SimpTheoremsArray_isDeclToUnfold___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__23; lean_object* l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*); lean_object* l_Lean_ScopedEnvExtension_addLocalEntry___rarg(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__4; LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_addConst(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_registerBuiltinAttribute(lean_object*, lean_object*); lean_object* l_Array_back___rarg(lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__12; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_SimpTheoremsArray_eraseTheorem___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__7; LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__5; lean_object* l_List_reverse___rarg(lean_object*); LEAN_EXPORT lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at_Lean_Meta_addSimpTheoremEntry___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -490,9 +489,11 @@ size_t lean_usize_sub(size_t, size_t); lean_object* l_Lean_mkHashMapImp___rarg(lean_object*); static lean_object* l_Lean_Meta_ppSimpTheorem___rarg___lambda__2___closed__1; static lean_object* l_Lean_Meta_instInhabitedSimpEntry___closed__1; +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__2; LEAN_EXPORT lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_mkSimpAttr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__12; 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*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__4; static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__9; LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_find_x3f___at_Lean_Meta_addSimpTheoremEntry___spec__2(lean_object*, lean_object*); size_t lean_usize_add(size_t, size_t); @@ -504,6 +505,8 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_ lean_object* l_Lean_Meta_mkEqFalse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_mapM_loop___at___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__27; +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__7; LEAN_EXPORT lean_object* l_Lean_Meta_simpExtensionMapRef; LEAN_EXPORT uint8_t l_Lean_Meta_SimpTheoremsArray_isLetDeclToUnfold(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_eraseAux___at_Lean_Meta_SimpTheorems_eraseCore___spec__2(lean_object*, size_t, lean_object*); @@ -512,10 +515,9 @@ lean_object* l_Lean_Expr_fvar___override(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheoremEntry___spec__1(lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Lean_PersistentHashMap_containsAtAux___at_Lean_Meta_SimpTheorems_isLemma___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__19; size_t lean_usize_shift_left(size_t, size_t); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__5; lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__14; static lean_object* l_Lean_Meta_instToFormatSimpTheorem___closed__5; lean_object* l_List_redLength___rarg(lean_object*); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_contains___at_Lean_Meta_SimpTheorems_isLemma___spec__1___boxed(lean_object*, lean_object*); @@ -537,13 +539,13 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_ lean_object* lean_array_get_size(lean_object*); static lean_object* l_Lean_Meta_ppOrigin___rarg___lambda__1___closed__5; LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5538____spec__1(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_instToFormatSimpTheorem(lean_object*); lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_SimpTheorems_toUnfoldThms___default___closed__1; LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_le(lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__24; -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__20; +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__8; uint8_t lean_usize_dec_lt(size_t, size_t); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Meta_addSimpTheoremEntry___spec__8(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at_Lean_Meta_addSimpTheoremEntry___spec__6(lean_object*, size_t, size_t, lean_object*, lean_object*); @@ -565,6 +567,7 @@ extern lean_object* l_Lean_PersistentHashMap_empty___at_Lean_Meta_Instances_eras uint8_t l_Lean_Expr_isFVar(lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___lambda__3___closed__8; uint8_t l_Lean_Expr_isForall(lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_eraseCore(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheoremsArray_addTheorem(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheorems_addDeclToUnfold___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -582,19 +585,15 @@ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insert___at_Lean_Meta_addSimpT LEAN_EXPORT lean_object* l_Lean_Meta_SimpTheoremsArray_eraseTheorem(lean_object*, lean_object*); uint64_t l_Lean_Meta_DiscrTree_Key_hash(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_shouldPreprocess___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__28; static lean_object* l_Lean_Meta_DiscrTree_insertCore___at_Lean_Meta_addSimpTheoremEntry___spec__1___closed__2; LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux_traverse___at_Lean_Meta_addSimpTheoremEntry___spec__7(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Nat_repr(lean_object*); static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__1; LEAN_EXPORT uint8_t l_Lean_PersistentHashMap_containsAux___at_Lean_Meta_SimpTheorems_erase___spec__2(lean_object*, size_t, lean_object*); -static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__4; static lean_object* l_Lean_PersistentHashMap_empty___at_Lean_Meta_SimpTheorems_lemmaNames___default___spec__1___closed__4; -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__12; size_t lean_usize_land(size_t, size_t); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at_Lean_Meta_addSimpTheoremEntry_updateLemmaNames___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_whnfR(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__27; static lean_object* l___private_Lean_Meta_Tactic_Simp_SimpTheorems_0__Lean_Meta_preprocess_go___closed__8; LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_SimpTheorems_eraseCore___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*); @@ -606,6 +605,7 @@ lean_object* l_Lean_throwError___at___private_Lean_Meta_InferType_0__Lean_Meta_i LEAN_EXPORT lean_object* l_Lean_Meta_instReprOrigin; uint8_t l_Array_isEmpty___rarg(lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_openAbstractMVarsResult___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__28; static lean_object* _init_l_Lean_Meta_instInhabitedOrigin___closed__1() { _start: { @@ -2385,7 +2385,7 @@ lean_ctor_set_uint8(x_4, 0, x_1); lean_ctor_set_uint8(x_4, 1, x_2); lean_ctor_set_uint8(x_4, 2, x_3); lean_ctor_set_uint8(x_4, 3, x_2); -lean_ctor_set_uint8(x_4, 4, x_2); +lean_ctor_set_uint8(x_4, 4, x_1); return x_4; } } @@ -13515,7 +13515,7 @@ x_15 = l_Lean_Meta_addSimpTheorem(x_1, x_2, x_12, x_13, x_14, x_6, x_7, x_8, x_9 return x_15; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1() { _start: { lean_object* x_1; @@ -13523,7 +13523,7 @@ x_1 = lean_mk_string_from_bytes("Lean", 4); return x_1; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__2() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__2() { _start: { lean_object* x_1; @@ -13531,7 +13531,7 @@ x_1 = lean_mk_string_from_bytes("Parser", 6); return x_1; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__3() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__3() { _start: { lean_object* x_1; @@ -13539,7 +13539,7 @@ x_1 = lean_mk_string_from_bytes("Tactic", 6); return x_1; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__4() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__4() { _start: { lean_object* x_1; @@ -13547,19 +13547,19 @@ x_1 = lean_mk_string_from_bytes("tacticSeq", 9); return x_1; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__5() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__2; -x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__3; -x_4 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__4; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__2; +x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__3; +x_4 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__4; x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4); return x_5; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__6() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__6() { _start: { lean_object* x_1; @@ -13567,19 +13567,19 @@ x_1 = lean_mk_string_from_bytes("tacticSeq1Indented", 18); return x_1; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__7() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__2; -x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__3; -x_4 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__6; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__2; +x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__3; +x_4 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__6; x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4); return x_5; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__8() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__8() { _start: { lean_object* x_1; @@ -13587,17 +13587,17 @@ x_1 = lean_mk_string_from_bytes("null", 4); return x_1; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__9() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__9() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__8; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__8; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__10() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__10() { _start: { lean_object* x_1; @@ -13605,41 +13605,41 @@ x_1 = lean_mk_string_from_bytes("exact", 5); return x_1; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__11() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__11() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__2; -x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__3; -x_4 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__10; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__2; +x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__3; +x_4 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__10; x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4); return x_5; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__12() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__12() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(2); -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__10; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__10; x_3 = lean_alloc_ctor(2, 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___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__13() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__13() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__12; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__12; x_3 = lean_array_push(x_1, x_2); return x_3; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__14() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__14() { _start: { lean_object* x_1; @@ -13647,7 +13647,7 @@ x_1 = lean_mk_string_from_bytes("Term", 4); return x_1; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__15() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__15() { _start: { lean_object* x_1; @@ -13655,19 +13655,19 @@ x_1 = lean_mk_string_from_bytes("declName", 8); return x_1; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__16() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__16() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__2; -x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__14; -x_4 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__15; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__2; +x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__14; +x_4 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__15; x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4); return x_5; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__17() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__17() { _start: { lean_object* x_1; @@ -13675,35 +13675,35 @@ x_1 = lean_mk_string_from_bytes("decl_name%", 10); return x_1; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__18() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__18() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(2); -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__17; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__17; x_3 = lean_alloc_ctor(2, 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___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__19() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__19() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__18; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__18; x_3 = lean_array_push(x_1, x_2); return x_3; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__20() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__20() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = lean_box(2); -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__16; -x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__19; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__16; +x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__19; x_4 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -13711,23 +13711,23 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__21() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__21() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__13; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__20; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__13; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__20; x_3 = lean_array_push(x_1, x_2); return x_3; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__22() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__22() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = lean_box(2); -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__11; -x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__21; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__11; +x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__21; x_4 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -13735,23 +13735,23 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__23() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__23() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__22; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__22; x_3 = lean_array_push(x_1, x_2); return x_3; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__24() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__24() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = lean_box(2); -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__9; -x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__23; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__9; +x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__23; x_4 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -13759,23 +13759,23 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__25() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__25() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__24; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__24; x_3 = lean_array_push(x_1, x_2); return x_3; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__26() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__26() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = lean_box(2); -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__7; -x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__25; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__7; +x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__25; x_4 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -13783,23 +13783,23 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__27() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__27() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Meta_SimpTheorem_keys___default___closed__1; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__26; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__26; x_3 = lean_array_push(x_1, x_2); return x_3; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__28() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__28() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = lean_box(2); -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__5; -x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__27; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__5; +x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__27; x_4 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -13807,11 +13807,11 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917_() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918_() { _start: { lean_object* x_1; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__28; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__28; return x_1; } } @@ -14795,9 +14795,9 @@ static lean_object* _init_l_Lean_Meta_mkSimpAttr___lambda__1___closed__15() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1; -x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__2; -x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__3; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1; +x_2 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__2; +x_3 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__3; x_4 = l_Lean_Meta_mkSimpAttr___lambda__1___closed__14; x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4); return x_5; @@ -15540,11 +15540,11 @@ lean_dec(x_1); return x_6; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5449_() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5450_() { _start: { lean_object* x_1; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__28; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__28; return x_1; } } @@ -15634,7 +15634,7 @@ x_7 = l_Lean_registerSimpleScopedEnvExtension___rarg(x_6, x_2); return x_7; } } -LEAN_EXPORT lean_object* l_Lean_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5537____spec__1(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5538____spec__1(lean_object* x_1) { _start: { lean_object* x_2; @@ -15642,7 +15642,7 @@ x_2 = l_Lean_mkHashMapImp___rarg(x_1); return x_2; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5537_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5538_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; @@ -15669,20 +15669,20 @@ return x_8; } } } -LEAN_EXPORT lean_object* l_Lean_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5537____spec__1___boxed(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5538____spec__1___boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_Lean_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5537____spec__1(x_1); +x_2 = l_Lean_mkHashMap___at_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5538____spec__1(x_1); lean_dec(x_1); return x_2; } } -static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5573_() { +static lean_object* _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5574_() { _start: { lean_object* x_1; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__28; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__28; return x_1; } } @@ -16127,7 +16127,7 @@ x_4 = lean_box(x_3); return x_4; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__1() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__1() { _start: { lean_object* x_1; @@ -16135,17 +16135,17 @@ x_1 = lean_mk_string_from_bytes("simp", 4); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__2() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____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_SimpTheorems___hyg_5673____closed__1; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__1; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__3() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__3() { _start: { lean_object* x_1; @@ -16153,7 +16153,7 @@ x_1 = lean_mk_string_from_bytes("Meta", 4); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__4() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__4() { _start: { lean_object* x_1; @@ -16161,18 +16161,18 @@ x_1 = lean_mk_string_from_bytes("simpExtension", 13); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__5() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__3; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__4; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__3; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__4; x_4 = l_Lean_Name_mkStr3(x_1, x_2, x_3); return x_4; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__6() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__6() { _start: { lean_object* x_1; @@ -16180,18 +16180,18 @@ x_1 = lean_mk_string_from_bytes("simplification theorem", 22); return x_1; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__2; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__6; -x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__5; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__2; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__6; +x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__5; x_5 = l_Lean_Meta_registerSimpAttr(x_2, x_3, x_4, x_1); return x_5; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__1() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__1() { _start: { lean_object* x_1; @@ -16199,17 +16199,17 @@ x_1 = lean_mk_string_from_bytes("seval", 5); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__2() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____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_SimpTheorems___hyg_5699____closed__1; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__1; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__3() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__3() { _start: { lean_object* x_1; @@ -16217,18 +16217,18 @@ x_1 = lean_mk_string_from_bytes("sevalSimpExtension", 18); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__4() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__3; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__3; +x_1 = l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__3; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__3; x_4 = l_Lean_Name_mkStr3(x_1, x_2, x_3); return x_4; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__5() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__5() { _start: { lean_object* x_1; @@ -16236,13 +16236,13 @@ x_1 = lean_mk_string_from_bytes("symbolic evaluator theorem", 26); return x_1; } } -LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__2; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__5; -x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__4; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__2; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__5; +x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__4; x_5 = l_Lean_Meta_registerSimpAttr(x_2, x_3, x_4, x_1); return x_5; } @@ -19030,64 +19030,64 @@ l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__ lean_mark_persistent(l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__15); l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__16 = _init_l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__16(); lean_mark_persistent(l_Lean_ScopedEnvExtension_add___at_Lean_Meta_addSimpTheorem___spec__1___closed__16); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__1); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__2 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__2(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__2); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__3 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__3(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__3); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__4 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__4(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__4); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__5 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__5(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__5); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__6 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__6(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__6); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__7 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__7(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__7); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__8 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__8(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__8); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__9 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__9(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__9); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__10 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__10(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__10); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__11 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__11(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__11); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__12 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__12(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__12); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__13 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__13(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__13); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__14 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__14(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__14); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__15 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__15(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__15); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__16 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__16(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__16); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__17 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__17(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__17); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__18 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__18(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__18); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__19 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__19(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__19); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__20 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__20(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__20); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__21 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__21(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__21); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__22 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__22(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__22); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__23 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__23(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__23); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__24 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__24(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__24); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__25 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__25(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__25); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__26 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__26(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__26); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__27 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__27(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__27); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__28 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__28(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917____closed__28); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917_ = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917_(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4917_); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__1); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__2 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__2(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__2); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__3 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__3(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__3); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__4 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__4(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__4); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__5 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__5(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__5); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__6 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__6(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__6); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__7 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__7(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__7); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__8 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__8(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__8); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__9 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__9(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__9); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__10 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__10(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__10); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__11 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__11(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__11); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__12 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__12(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__12); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__13 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__13(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__13); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__14 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__14(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__14); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__15 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__15(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__15); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__16 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__16(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__16); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__17 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__17(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__17); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__18 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__18(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__18); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__19 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__19(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__19); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__20 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__20(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__20); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__21 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__21(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__21); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__22 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__22(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__22); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__23 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__23(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__23); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__24 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__24(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__24); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__25 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__25(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__25); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__26 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__26(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__26); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__27 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__27(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__27); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__28 = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__28(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918____closed__28); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918_ = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918_(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_4918_); l_Lean_Meta_mkSimpAttr___lambda__1___closed__1 = _init_l_Lean_Meta_mkSimpAttr___lambda__1___closed__1(); lean_mark_persistent(l_Lean_Meta_mkSimpAttr___lambda__1___closed__1); l_Lean_Meta_mkSimpAttr___lambda__1___closed__2 = _init_l_Lean_Meta_mkSimpAttr___lambda__1___closed__2(); @@ -19118,51 +19118,51 @@ l_Lean_Meta_mkSimpAttr___lambda__1___closed__14 = _init_l_Lean_Meta_mkSimpAttr__ lean_mark_persistent(l_Lean_Meta_mkSimpAttr___lambda__1___closed__14); l_Lean_Meta_mkSimpAttr___lambda__1___closed__15 = _init_l_Lean_Meta_mkSimpAttr___lambda__1___closed__15(); lean_mark_persistent(l_Lean_Meta_mkSimpAttr___lambda__1___closed__15); -l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5449_ = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5449_(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5449_); +l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5450_ = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5450_(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5450_); l_Lean_Meta_mkSimpExt___closed__1 = _init_l_Lean_Meta_mkSimpExt___closed__1(); lean_mark_persistent(l_Lean_Meta_mkSimpExt___closed__1); l_Lean_Meta_mkSimpExt___closed__2 = _init_l_Lean_Meta_mkSimpExt___closed__2(); lean_mark_persistent(l_Lean_Meta_mkSimpExt___closed__2); l_Lean_Meta_mkSimpExt___closed__3 = _init_l_Lean_Meta_mkSimpExt___closed__3(); lean_mark_persistent(l_Lean_Meta_mkSimpExt___closed__3); -if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5537_(lean_io_mk_world()); +if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5538_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Meta_simpExtensionMapRef = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Meta_simpExtensionMapRef); lean_dec_ref(res); -}l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5573_ = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5573_(); -lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5573_); +}l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5574_ = _init_l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5574_(); +lean_mark_persistent(l___auto____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5574_); l_Lean_Meta_registerSimpAttr___closed__1 = _init_l_Lean_Meta_registerSimpAttr___closed__1(); lean_mark_persistent(l_Lean_Meta_registerSimpAttr___closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__1(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__2(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__3(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__3); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__4(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__4); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__5(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__5); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__6 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__6(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673____closed__6); -if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5673_(lean_io_mk_world()); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__1(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__1); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__2(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__2); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__3(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__3); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__4(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__4); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__5(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__5); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__6 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__6(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674____closed__6); +if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5674_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Meta_simpExtension = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Meta_simpExtension); lean_dec_ref(res); -}l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__1(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__2(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__3(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__3); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__4(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__4); -l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__5(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699____closed__5); -if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5699_(lean_io_mk_world()); +}l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__1(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__1); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__2(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__2); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__3(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__3); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__4(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__4); +l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__5(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700____closed__5); +if (builtin) {res = l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpTheorems___hyg_5700_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Meta_sevalSimpExtension = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Meta_sevalSimpExtension); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Simp/Types.c b/stage0/stdlib/Lean/Meta/Tactic/Simp/Types.c index c410d26728..9776354e81 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Simp/Types.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Simp/Types.c @@ -141,7 +141,6 @@ LEAN_EXPORT uint32_t l_Lean_Meta_Simp_Context_dischargeDepth___default; LEAN_EXPORT lean_object* l_Lean_HashMap_insert___at_Lean_Meta_Simp_recordSimpTheorem___spec__3(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_getConfig___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_AssocList_foldlM___at_Lean_Meta_Simp_recordSimpTheorem___spec__6___at_Lean_Meta_Simp_recordSimpTheorem___spec__7(lean_object*, lean_object*); -static lean_object* l_Lean_Meta_Simp_getDtConfig___closed__3; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_congrArgs___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_Simp_Context_config___default___closed__1; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___spec__2___lambda__3___boxed(lean_object**); @@ -205,7 +204,6 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_tryAutoCon LEAN_EXPORT lean_object* l_Lean_Meta_Simp_instInhabitedMethods___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_panic___at_Lean_Expr_appFn_x21___spec__1(lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_mkCongrSimp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_Simp_getDtConfig___closed__1; static lean_object* l_Lean_Meta_Simp_removeUnnecessaryCasts_isDummyEqRec___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_Simp_mkEqTransResultStep(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_name_eq(lean_object*, lean_object*); @@ -248,7 +246,6 @@ static lean_object* l_Lean_isTracingEnabledFor___at_Lean_Meta_Simp_congrArgs___s lean_object* l_Lean_Meta_SimpExtension_getTheorems(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_congrArgs___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Simp_Methods_pre___default___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Meta_Simp_getDtConfig___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_Simp_instInhabitedMethods___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_Simp_removeUnnecessaryCasts_isDummyEqRec___closed__5; lean_object* l_Lean_Meta_mkCongr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -978,7 +975,7 @@ lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 12, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 13, x_4); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 14, x_3); lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 15, x_3); -lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_4); +lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 16, x_3); return x_6; } } @@ -19948,54 +19945,6 @@ x_25 = l_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___lambda__4(x_1, x_2, x_3, x_4, return x_25; } } -static lean_object* _init_l_Lean_Meta_Simp_getDtConfig___closed__1() { -_start: -{ -uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4; -x_1 = 0; -x_2 = 0; -x_3 = 1; -x_4 = lean_alloc_ctor(0, 0, 5); -lean_ctor_set_uint8(x_4, 0, x_1); -lean_ctor_set_uint8(x_4, 1, x_1); -lean_ctor_set_uint8(x_4, 2, x_2); -lean_ctor_set_uint8(x_4, 3, x_1); -lean_ctor_set_uint8(x_4, 4, x_3); -return x_4; -} -} -static lean_object* _init_l_Lean_Meta_Simp_getDtConfig___closed__2() { -_start: -{ -uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4; -x_1 = 0; -x_2 = 0; -x_3 = 1; -x_4 = lean_alloc_ctor(0, 0, 5); -lean_ctor_set_uint8(x_4, 0, x_1); -lean_ctor_set_uint8(x_4, 1, x_1); -lean_ctor_set_uint8(x_4, 2, x_2); -lean_ctor_set_uint8(x_4, 3, x_3); -lean_ctor_set_uint8(x_4, 4, x_3); -return x_4; -} -} -static lean_object* _init_l_Lean_Meta_Simp_getDtConfig___closed__3() { -_start: -{ -uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4; -x_1 = 0; -x_2 = 1; -x_3 = 0; -x_4 = lean_alloc_ctor(0, 0, 5); -lean_ctor_set_uint8(x_4, 0, x_1); -lean_ctor_set_uint8(x_4, 1, x_2); -lean_ctor_set_uint8(x_4, 2, x_3); -lean_ctor_set_uint8(x_4, 3, x_1); -lean_ctor_set_uint8(x_4, 4, x_2); -return x_4; -} -} LEAN_EXPORT lean_object* l_Lean_Meta_Simp_getDtConfig(lean_object* x_1) { _start: { @@ -20003,36 +19952,60 @@ uint8_t x_2; x_2 = lean_ctor_get_uint8(x_1, sizeof(void*)*2 + 4); if (x_2 == 0) { -uint8_t x_3; +uint8_t x_3; uint8_t x_4; uint8_t x_5; uint8_t x_6; lean_object* x_7; x_3 = lean_ctor_get_uint8(x_1, sizeof(void*)*2 + 3); -if (x_3 == 0) -{ -lean_object* x_4; -x_4 = l_Lean_Meta_Simp_getDtConfig___closed__1; -return x_4; -} -else -{ -lean_object* x_5; -x_5 = l_Lean_Meta_Simp_getDtConfig___closed__2; -return x_5; -} -} -else -{ -uint8_t x_6; -x_6 = lean_ctor_get_uint8(x_1, sizeof(void*)*2 + 3); -if (x_6 == 0) -{ -lean_object* x_7; -x_7 = l_Lean_Meta_Simp_getDtConfig___closed__3; +x_4 = lean_ctor_get_uint8(x_1, sizeof(void*)*2 + 16); +x_5 = 0; +x_6 = 0; +x_7 = lean_alloc_ctor(0, 0, 5); +lean_ctor_set_uint8(x_7, 0, x_5); +lean_ctor_set_uint8(x_7, 1, x_2); +lean_ctor_set_uint8(x_7, 2, x_6); +lean_ctor_set_uint8(x_7, 3, x_3); +lean_ctor_set_uint8(x_7, 4, x_4); return x_7; } else { -lean_object* x_8; -x_8 = l_Lean_Meta_simpDtConfig; -return x_8; +uint8_t x_8; +x_8 = lean_ctor_get_uint8(x_1, sizeof(void*)*2 + 3); +if (x_8 == 0) +{ +uint8_t x_9; uint8_t x_10; uint8_t x_11; lean_object* x_12; +x_9 = lean_ctor_get_uint8(x_1, sizeof(void*)*2 + 16); +x_10 = 0; +x_11 = 0; +x_12 = lean_alloc_ctor(0, 0, 5); +lean_ctor_set_uint8(x_12, 0, x_10); +lean_ctor_set_uint8(x_12, 1, x_2); +lean_ctor_set_uint8(x_12, 2, x_11); +lean_ctor_set_uint8(x_12, 3, x_8); +lean_ctor_set_uint8(x_12, 4, x_9); +return x_12; +} +else +{ +uint8_t x_13; +x_13 = lean_ctor_get_uint8(x_1, sizeof(void*)*2 + 16); +if (x_13 == 0) +{ +lean_object* x_14; +x_14 = l_Lean_Meta_simpDtConfig; +return x_14; +} +else +{ +uint8_t x_15; uint8_t x_16; lean_object* x_17; +x_15 = 0; +x_16 = 0; +x_17 = lean_alloc_ctor(0, 0, 5); +lean_ctor_set_uint8(x_17, 0, x_15); +lean_ctor_set_uint8(x_17, 1, x_2); +lean_ctor_set_uint8(x_17, 2, x_16); +lean_ctor_set_uint8(x_17, 3, x_8); +lean_ctor_set_uint8(x_17, 4, x_13); +return x_17; +} } } } @@ -21101,12 +21074,6 @@ l_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___lambda__5___closed__4 = _init_l_Lean_ lean_mark_persistent(l_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___lambda__5___closed__4); l_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___lambda__5___closed__5 = _init_l_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___lambda__5___closed__5(); lean_mark_persistent(l_Lean_Meta_Simp_tryAutoCongrTheorem_x3f___lambda__5___closed__5); -l_Lean_Meta_Simp_getDtConfig___closed__1 = _init_l_Lean_Meta_Simp_getDtConfig___closed__1(); -lean_mark_persistent(l_Lean_Meta_Simp_getDtConfig___closed__1); -l_Lean_Meta_Simp_getDtConfig___closed__2 = _init_l_Lean_Meta_Simp_getDtConfig___closed__2(); -lean_mark_persistent(l_Lean_Meta_Simp_getDtConfig___closed__2); -l_Lean_Meta_Simp_getDtConfig___closed__3 = _init_l_Lean_Meta_Simp_getDtConfig___closed__3(); -lean_mark_persistent(l_Lean_Meta_Simp_getDtConfig___closed__3); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus