From 855a762bcb6ab7be3adcdf793d654f153a71fe56 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Feb 2024 06:38:56 -0800 Subject: [PATCH] chore: update stage0 --- stage0/stdlib/Init/Tactics.c | 95 ++ stage0/stdlib/Lean/Data/Position.c | 10 +- stage0/stdlib/Lean/Elab/Tactic/NormCast.c | 1556 +++++++++++++++++++++ stage0/stdlib/Lean/Meta/Tactic/NormCast.c | 4 +- stage0/stdlib/Lean/Meta/Tactic/TryThis.c | 55 +- 5 files changed, 1713 insertions(+), 7 deletions(-) diff --git a/stage0/stdlib/Init/Tactics.c b/stage0/stdlib/Init/Tactics.c index f3dfb74417..d90d5659af 100644 --- a/stage0/stdlib/Init/Tactics.c +++ b/stage0/stdlib/Init/Tactics.c @@ -682,6 +682,7 @@ static lean_object* l_Lean_Parser_Tactic_rwRule___closed__14; static lean_object* l_Lean_Parser_Tactic_tacticStop_____closed__4; static lean_object* l_Lean_Parser_Tactic_simpTrace___closed__10; static lean_object* l_Lean_Parser_Tactic_simpAll___closed__13; +static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__4; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_simpa; static lean_object* l_Lean_Parser_Tactic_discharger___closed__13; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_injection; @@ -698,6 +699,7 @@ static lean_object* l_Lean_Parser_Tactic_tacticSimpa_x3f_x21_____closed__3; static lean_object* l_Lean_Parser_Tactic_pushCast___closed__11; static lean_object* l_Lean_Parser_Tactic_rwRule___closed__3; static lean_object* l_Lean_Parser_Tactic_first___closed__23; +static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__5; static lean_object* l_Lean_Parser_Tactic_tacticHave_____closed__9; static lean_object* l_Lean_Parser_Tactic_split___closed__7; static lean_object* l_Lean_Parser_Tactic_rotateLeft___closed__11; @@ -922,6 +924,7 @@ static lean_object* l_Lean_Parser_Tactic_tacticSimp_x3f_x21_____closed__5; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_simpPre; static lean_object* l_Lean_Parser_Tactic_first___closed__21; static lean_object* l_Lean_Parser_Tactic_unfold___closed__6; +static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__1; static lean_object* l_Lean_Parser_Tactic_rotateRight___closed__4; static lean_object* l_Lean_Parser_Tactic_traceState___closed__5; static lean_object* l_Lean_Parser_Tactic_simp___closed__1; @@ -1085,6 +1088,7 @@ static lean_object* l_Lean_Parser_Tactic_simpa___closed__6; static lean_object* l_Lean_Parser_Tactic_cases___closed__2; static lean_object* l_Lean_Parser_Tactic_locationHyp___closed__17; static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticShow____1___closed__2; +static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__6; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_simp; static lean_object* l_Lean_Parser_Tactic_pushCast___closed__9; static lean_object* l_Lean_Parser_Tactic_split___closed__8; @@ -1122,6 +1126,7 @@ static lean_object* l_Lean_Parser_Tactic_withAnnotateState___closed__1; static lean_object* l_Lean_Parser_Tactic_contradiction___closed__2; static lean_object* l_Lean_Parser_Tactic_discharger___closed__2; static lean_object* l_Lean_Parser_Tactic_letrec___closed__12; +static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__3; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRfl__1(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_Tactic_simpTraceArgsRest___closed__1; static lean_object* l_Lean_Parser_Tactic_simpLemma___closed__3; @@ -1263,6 +1268,7 @@ static lean_object* l_Lean_Parser_Tactic_rwRuleSeq___closed__3; static lean_object* l_Lean_Parser_Tactic_focus___closed__6; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticSimpa_x3f_x21____1(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_omega; +static lean_object* l_Lean_Parser_Tactic_normCastAddElim___closed__2; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_clear; static lean_object* l_Lean_Parser_Tactic_locationHyp___closed__3; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_traceState; @@ -1278,6 +1284,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_exact; static lean_object* l_Lean_Parser_Tactic_traceMessage___closed__2; static lean_object* l_Lean_Parser_Tactic_tacticTry_____closed__3; static lean_object* l_Lean_Parser_Tactic_omega___closed__5; +LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_normCastAddElim; static lean_object* l_Lean_Parser_Tactic_paren___closed__2; static lean_object* l_Lean_Parser_Tactic_discharger___closed__1; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_simpArgs; @@ -19977,6 +19984,80 @@ x_1 = l_Lean_Parser_Tactic_pushCast___closed__14; return x_1; } } +static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("normCastAddElim", 15); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__1; +x_2 = l_Lean_Parser_Tactic_withAnnotateState___closed__2; +x_3 = l_Lean_Parser_Tactic_withAnnotateState___closed__3; +x_4 = l_Lean_Parser_Tactic_normCastAddElim___closed__1; +x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4); +return x_5; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("norm_cast_add_elim", 18); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Tactic_normCastAddElim___closed__3; +x_2 = lean_alloc_ctor(5, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__7; +x_2 = l_Lean_Parser_Tactic_normCastAddElim___closed__4; +x_3 = l_Lean_Parser_Tactic_intros___closed__8; +x_4 = lean_alloc_ctor(2, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_normCastAddElim___closed__2; +x_2 = lean_unsigned_to_nat(1022u); +x_3 = l_Lean_Parser_Tactic_normCastAddElim___closed__5; +x_4 = lean_alloc_ctor(3, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_normCastAddElim() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_Tactic_normCastAddElim___closed__6; +return x_1; +} +} static lean_object* _init_l_Lean_Parser_Attr_simp___closed__1() { _start: { @@ -24353,6 +24434,20 @@ l_Lean_Parser_Tactic_pushCast___closed__14 = _init_l_Lean_Parser_Tactic_pushCast lean_mark_persistent(l_Lean_Parser_Tactic_pushCast___closed__14); l_Lean_Parser_Tactic_pushCast = _init_l_Lean_Parser_Tactic_pushCast(); lean_mark_persistent(l_Lean_Parser_Tactic_pushCast); +l_Lean_Parser_Tactic_normCastAddElim___closed__1 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__1); +l_Lean_Parser_Tactic_normCastAddElim___closed__2 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__2); +l_Lean_Parser_Tactic_normCastAddElim___closed__3 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__3); +l_Lean_Parser_Tactic_normCastAddElim___closed__4 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__4); +l_Lean_Parser_Tactic_normCastAddElim___closed__5 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__5(); +lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__5); +l_Lean_Parser_Tactic_normCastAddElim___closed__6 = _init_l_Lean_Parser_Tactic_normCastAddElim___closed__6(); +lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim___closed__6); +l_Lean_Parser_Tactic_normCastAddElim = _init_l_Lean_Parser_Tactic_normCastAddElim(); +lean_mark_persistent(l_Lean_Parser_Tactic_normCastAddElim); l_Lean_Parser_Attr_simp___closed__1 = _init_l_Lean_Parser_Attr_simp___closed__1(); lean_mark_persistent(l_Lean_Parser_Attr_simp___closed__1); l_Lean_Parser_Attr_simp___closed__2 = _init_l_Lean_Parser_Attr_simp___closed__2(); diff --git a/stage0/stdlib/Lean/Data/Position.c b/stage0/stdlib/Lean/Data/Position.c index 38a6795ccc..fc92b0acb1 100644 --- a/stage0/stdlib/Lean/Data/Position.c +++ b/stage0/stdlib/Lean/Data/Position.c @@ -25,7 +25,6 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*); lean_object* l_Lean_mkAppN(lean_object*, lean_object*); static lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_176____closed__2; static lean_object* l___private_Lean_Data_Position_0__Lean_reprPosition____x40_Lean_Data_Position___hyg_176____closed__13; -lean_object* l_String_Iterator_pos(lean_object*); static lean_object* l_Lean_Position_instToFormatPosition___closed__2; LEAN_EXPORT lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*); static lean_object* l_Lean_Position_lt___closed__2; @@ -1182,7 +1181,8 @@ x_14 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_14, 0, x_6); lean_ctor_set(x_14, 1, x_13); x_15 = l_String_Iterator_nextn(x_14, x_10); -x_16 = l_String_Iterator_pos(x_15); +x_16 = lean_ctor_get(x_15, 1); +lean_inc(x_16); lean_dec(x_15); return x_16; } @@ -1195,7 +1195,8 @@ x_18 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_18, 0, x_6); lean_ctor_set(x_18, 1, x_17); x_19 = l_String_Iterator_nextn(x_18, x_10); -x_20 = l_String_Iterator_pos(x_19); +x_20 = lean_ctor_get(x_19, 1); +lean_inc(x_20); lean_dec(x_19); return x_20; } @@ -1213,7 +1214,8 @@ x_23 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_23, 0, x_6); lean_ctor_set(x_23, 1, x_22); x_24 = l_String_Iterator_nextn(x_23, x_21); -x_25 = l_String_Iterator_pos(x_24); +x_25 = lean_ctor_get(x_24, 1); +lean_inc(x_25); lean_dec(x_24); return x_25; } diff --git a/stage0/stdlib/Lean/Elab/Tactic/NormCast.c b/stage0/stdlib/Lean/Elab/Tactic/NormCast.c index 575859cef7..c0e5b1a998 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/NormCast.c +++ b/stage0/stdlib/Lean/Elab/Tactic/NormCast.c @@ -13,11 +13,13 @@ #ifdef __cplusplus extern "C" { #endif +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__19; lean_object* l_Lean_Meta_Simp_mkCongrFun(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__3___closed__3; lean_object* l_Lean_Expr_const___override(lean_object*, lean_object*); lean_object* l_Lean_Meta_getCoeFnInfo_x3f(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* lean_format_pretty(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__8___closed__1; static lean_object* l_Lean_Elab_Tactic_NormCast_evalNormCast0___closed__1; static lean_object* l_Lean_Elab_Tactic_NormCast_proveEqUsing___closed__1; @@ -34,11 +36,14 @@ static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__10___closed__2; lean_object* lean_mk_empty_array_with_capacity(lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__19; static lean_object* l_Lean_Elab_Tactic_NormCast_isCoeOf_x3f___closed__1; +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__4; static lean_object* l_Lean_Elab_Tactic_NormCast_upwardAndElim___closed__1; lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_evalPushCast___closed__1; +LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast_declRange___closed__4; static lean_object* l_Lean_Elab_Tactic_NormCast_isNumeral_x3f___closed__9; +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__5; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_isNumeral_x3f___closed__3; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__11(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -47,18 +52,23 @@ uint32_t l_UInt32_ofNatTruncate(lean_object*); lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___at_Lean_Meta_Simp_simpGround___spec__2___rarg(lean_object*, lean_object*); double lean_float_div(double, double); static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__10; +lean_object* l_List_mapTR_loop___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__5; static lean_object* l_Lean_Elab_Tactic_NormCast_evalNormCast0___closed__3; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_proveEqUsing___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* l_Lean_Syntax_formatStxAux(lean_object*, uint8_t, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_prove___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__21; 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_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_NormCast_evalNormCast0___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_prove___spec__1___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3; +static lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__3; lean_object* l_Lean_Elab_Tactic_expandOptLocation(lean_object*); lean_object* l_Lean_Elab_Tactic_expandLocation(lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__12; @@ -69,14 +79,22 @@ extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute; static lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure___lambda__3___closed__1; LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabModCast_declRange(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_isCoeOf_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure___lambda__1___closed__7; lean_object* lean_array_push(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_isNumeral_x3f___closed__8; static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__6___closed__10; +lean_object* l_Lean_instBEqLocalInstance___boxed(lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__8; static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__10___closed__3; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__11; uint8_t lean_usize_dec_eq(size_t, size_t); static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__6___closed__1; +static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__3; static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__11___closed__2; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__33; +lean_object* l_Lean_replaceRef(lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__7; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0_declRange___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_proveEqUsingDown(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_instantiateMVars___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -90,8 +108,11 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_prove___lambda__1___boxed(l lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_numeralToCoe___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0(lean_object*); +LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_elabModCast___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__2; static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__6___closed__2; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__6; uint8_t lean_float_decLt(double, double); lean_object* l_Lean_Meta_Simp_rewrite_x3f(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0_declRange___closed__6; @@ -99,8 +120,10 @@ lean_object* l_Lean_addBuiltinDeclarationRanges(lean_object*, lean_object*, lean LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_proveEqUsingDown___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_withSeconds___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast_declRange___closed__3; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__9; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_proveEqUsing___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__25; uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*); lean_object* l_Lean_Name_mkStr5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_Simp_DischargeWrapper_with___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -110,22 +133,30 @@ lean_object* l_Lean_stringToMessageData(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__21; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabModCast___closed__2; +lean_object* l_List_filterMap___at_Lean_resolveGlobalConst___spec__1(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0___closed__3; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__24; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__2___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast_declRange___closed__6; lean_object* l_Lean_Meta_SimpExtension_getTheorems___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__3; lean_object* l_Lean_Elab_Tactic_getFVarIds(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_prove___lambda__1___closed__1; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0___closed__4; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_prove___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_string_dec_eq(lean_object*, lean_object*); +lean_object* l_List_toString___at_Lean_resolveGlobalConstNoOverloadCore___spec__2(lean_object*); +extern lean_object* l_Lean_Expr_instBEqExpr; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabModCast___closed__3; static lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure___lambda__1___closed__4; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_instBEqProd___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_getSimpCongrTheorems___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__2___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0_declRange___closed__5; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__27; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabModCast_declRange___closed__3; static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__11___closed__4; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -133,38 +164,47 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0___clo static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0_declRange___closed__3; static lean_object* l_Lean_Elab_Tactic_NormCast_numeralToCoe___lambda__1___closed__2; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabModCast_declRange___closed__7; +lean_object* l_instHashableArray___rarg___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__2___lambda__2(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, uint8_t, double, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__20; static lean_object* l_Lean_Elab_Tactic_NormCast_mkCoe___closed__2; static lean_object* l_Lean_Elab_Tactic_NormCast_prove___lambda__1___closed__2; +LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0_declRange___closed__7; size_t lean_usize_of_nat(lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure___lambda__1___closed__6; lean_object* l_Lean_MVarId_getNondepPropHyps(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_List_mapTR_loop___at_Lean_resolveGlobalConstCore___spec__2(lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast___closed__1; lean_object* l_Lean_Meta_findLocalDeclWithType_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__8___closed__3; static lean_object* l_Lean_Elab_Tactic_NormCast_elabModCast___closed__2; static uint32_t l_Lean_Elab_Tactic_NormCast_proveEqUsing___closed__2; +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__3(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, uint8_t, double, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_prove___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0_declRange___closed__2; lean_object* l_Lean_throwError___at_Lean_Expr_abstractRangeM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_withExpectedType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__5___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_ref_take(lean_object*, lean_object*); lean_object* l_Lean_Expr_getRevArg_x21(lean_object*, lean_object*); lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___at_Lean_Meta_processPostponed___spec__2___rarg(lean_object*, lean_object*); +extern lean_object* l_Lean_Elab_Command_commandElabAttribute; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabModCast_declRange___closed__2; uint8_t lean_nat_dec_eq(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__6___closed__5; static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__7; uint8_t lean_expr_eqv(lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__12; +LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_isNumeral_x3f___closed__5; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalConvNormCast___closed__6; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast___closed__5; lean_object* l_Lean_Meta_Simp_Result_mkEqSymm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_mkCoe(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabAuxDef___spec__1___rarg(lean_object*); lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabForall___spec__1___rarg(lean_object*); LEAN_EXPORT lean_object* l_MonadExcept_ofExcept___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_MVarId_getType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -176,11 +216,17 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalConvNormCast___ lean_object* l_Lean_registerTraceClass(lean_object*, uint8_t, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_prove___spec__1___lambda__4(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, uint8_t, double, 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_Elab_Tactic_Conv_getLhs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__14; +static lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__1; lean_object* l_Lean_Meta_simp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_elabModCast___closed__1; static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__6___closed__7; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_prove___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PersistentArray_append___rarg(lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__32; +lean_object* l_Lean_Meta_NormCast_addElim(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_MonadExcept_ofExcept___at_Lean_Elab_Tactic_NormCast_prove___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast___closed__3; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__2___lambda__3(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, uint8_t, double, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -191,10 +237,12 @@ lean_object* l_Lean_Elab_Tactic_withMainContext___rarg(lean_object*, lean_object static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__2; LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast_declRange(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_isCoeOf_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_bombEmoji; extern lean_object* l_Lean_checkEmoji; lean_object* lean_st_ref_get(lean_object*, lean_object*); static lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__3___closed__7; +uint8_t l_List_isEmpty___rarg(lean_object*); LEAN_EXPORT lean_object* l_Lean_withSeconds___at_Lean_Elab_Tactic_NormCast_prove___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_mk_ref(lean_object*, lean_object*); static double l_Lean_withSeconds___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__2___closed__1; @@ -211,16 +259,24 @@ static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_N lean_object* l_Lean_isTracingEnabledFor___at_Lean_Meta_Simp_congrArgs___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__2___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_numeralToCoe(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Expr_instHashableExpr; lean_object* l_Lean_Meta_Simp_Result_mkCast(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_io_mono_nanos_now(lean_object*); +LEAN_EXPORT lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_isNumeral_x3f___closed__4; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__13; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalConvNormCast___closed__4; +static lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__2; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__4___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_Elab_Tactic_NormCast_proveEqUsingDown___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_isNumeral_x3f___closed__6; static lean_object* l_Lean_Elab_Tactic_NormCast_elabModCast___lambda__2___closed__2; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalConvNormCast_declRange___closed__6; +lean_object* l_Lean_instHashableLocalInstance___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__9(lean_object*, lean_object*, lean_object*, uint32_t, lean_object*, lean_object*, uint32_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__2; +lean_object* l_instHashableProd___rarg___boxed(lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7; lean_object* l_Lean_Name_str___override(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__11___closed__3; LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -230,6 +286,7 @@ extern lean_object* l_Lean_Meta_NormCast_pushCastExt; static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__16; uint8_t l_Lean_Option_get___at___private_Lean_Util_Profile_0__Lean_get__profiler___spec__1(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__6___closed__6; +static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__2; lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__6___closed__8; static lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__3___closed__2; @@ -238,9 +295,12 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalConvNormCast_de LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__4(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_withTraceNode___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_throwTypeMismatchError___rarg(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_resolveGlobalName___at_Lean_Elab_Tactic_mkSimpOnly___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast_declRange___closed__5; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure___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_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_isCoeOf_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__26; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__16; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_prove___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_simpLocation(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_elabModCast___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -248,8 +308,12 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast_declRa lean_object* l_Lean_Elab_Tactic_mkSimpContext___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__10___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_evalNormCast0___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Std_Format_defWidth; static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__6___closed__4; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__29; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_isCoeOf_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__18; +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_evalNormCast0___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_evalPushCast___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*); @@ -265,10 +329,13 @@ LEAN_EXPORT lean_object* l_MonadExcept_ofExcept___at_Lean_Elab_Tactic_NormCast_s LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__11___boxed__const__1; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_prove___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SimpExtension_getTheorems(lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__1; extern lean_object* l_Lean_Meta_NormCast_normCastExt; double l_Float_ofScientific(lean_object*, uint8_t, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_prove___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_MetaM_run_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_evalConvNormCast___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__30; extern lean_object* l_Lean_crossEmoji; static lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__4___closed__1; static lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__3___closed__4; @@ -292,19 +359,24 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast_declRa LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_evalPushCast___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalConvNormCast_declRange___closed__7; static lean_object* l_Lean_Elab_Tactic_NormCast_evalNormCast0___lambda__4___closed__1; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__5; static lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__4___closed__2; static lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__3___closed__5; lean_object* l_Lean_Expr_app___override(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast___closed__4; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__2___lambda__4(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2; static lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure___lambda__1___closed__3; lean_object* l_Lean_Meta_applySimpResultToLocalDecl(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_normCastTarget(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__3; static lean_object* l_Lean_Elab_Tactic_NormCast_prove___closed__1; +LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__5___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_float_to_string(double); 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_Lean_Elab_Tactic_NormCast_elabAddElim___closed__28; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__3___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___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_normCastHyp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -315,10 +387,12 @@ LEAN_EXPORT lean_object* l_Lean_withSeconds___at_Lean_Elab_Tactic_NormCast_prove static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__6___closed__3; static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__13; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalConvNormCast_declRange___closed__2; +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalExact___spec__1___rarg(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__2(lean_object*, uint32_t, 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_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_prove___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__5(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -331,14 +405,21 @@ lean_object* lean_nat_sub(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_proveEqUsingDown___lambda__1___closed__2; lean_object* l_Lean_Expr_getAppFn(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__31; +lean_object* l_Lean_Elab_Command_liftCoreM___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_Simp_mkCongr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_normCastTarget___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalConvNormCast___closed__1; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__10; +lean_object* l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_prove___spec__1___lambda__3(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, uint8_t, double, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__9; +lean_object* l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*); lean_object* l_Lean_Meta_mkNumeral(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__1; static lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure___lambda__1___closed__2; static lean_object* l_Lean_Elab_Tactic_NormCast_numeralToCoe___lambda__1___closed__3; +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_evalNormCast0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_elabModCast___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_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_evalNormCast0___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -355,6 +436,7 @@ static lean_object* l_Lean_Elab_Tactic_NormCast_proveEqUsing___closed__3; size_t lean_usize_add(size_t, size_t); static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__14; static lean_object* l_Lean_Elab_Tactic_NormCast_proveEqUsing___closed__4; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__20; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_upwardAndElim___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Meta_Simp_defaultMaxSteps; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_isNumeral_x3f___boxed(lean_object*); @@ -365,6 +447,7 @@ lean_object* lean_array_uget(lean_object*, size_t); lean_object* l_Lean_Expr_fvar___override(lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_numeralToCoe___lambda__1___closed__1; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_evalNormCast0___closed__4; extern lean_object* l_Lean_trace_profiler; lean_object* l_Lean_throwError___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -372,8 +455,12 @@ lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__11___closed__1; lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__8; +lean_object* lean_string_append(lean_object*, lean_object*); lean_object* l_Lean_isTracingEnabledFor___at_Lean_Meta_processPostponed_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_Simp_mkDefaultMethods(lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalNormCast0_declRange___closed__4; @@ -398,23 +485,34 @@ LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_pro uint8_t l_Lean_Exception_isRuntime(lean_object*); static lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__5___closed__1; LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_NormCast_evalNormCast0___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*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4; +lean_object* l_Array_instBEqArray___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_prove___spec__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_List_filterTR_loop___at_Lean_resolveGlobalConstCore___spec__1(lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__23; +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__6; +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__22; static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_evalConvNormCast___closed__3; static lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__8___closed__4; +static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1; LEAN_EXPORT lean_object* l_MonadExcept_ofExcept___at_Lean_Elab_Tactic_NormCast_prove___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_normCastHyp___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_replaceMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_isNumeral_x3f(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabModCast_declRange___closed__5; lean_object* l_Lean_Elab_Term_tryPostpone(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_simp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_splittingProcedure(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__17; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__15; static lean_object* l_Lean_Elab_Tactic_NormCast_proveEqUsingDown___lambda__1___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_elabModCast___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_NormCast_evalPushCast___closed__2; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_derive___lambda__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__4; static lean_object* l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__18; LEAN_EXPORT lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_splittingProcedure___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__3___closed__6; @@ -15358,6 +15456,1352 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1); return x_4; } } +LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; lean_object* x_8; uint8_t x_9; +x_7 = lean_ctor_get(x_4, 5); +x_8 = l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(x_1, x_2, x_3, x_4, x_5, x_6); +x_9 = !lean_is_exclusive(x_8); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; +x_10 = lean_ctor_get(x_8, 0); +lean_inc(x_7); +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_7); +lean_ctor_set(x_11, 1, x_10); +lean_ctor_set_tag(x_8, 1); +lean_ctor_set(x_8, 0, x_11); +return x_8; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; +x_12 = lean_ctor_get(x_8, 0); +x_13 = lean_ctor_get(x_8, 1); +lean_inc(x_13); +lean_inc(x_12); +lean_dec(x_8); +lean_inc(x_7); +x_14 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_14, 0, x_7); +lean_ctor_set(x_14, 1, x_12); +x_15 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_15, 0, x_14); +lean_ctor_set(x_15, 1, x_13); +return x_15; +} +} +} +LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +_start: +{ +uint8_t x_8; +x_8 = !lean_is_exclusive(x_5); +if (x_8 == 0) +{ +lean_object* x_9; lean_object* x_10; lean_object* x_11; +x_9 = lean_ctor_get(x_5, 5); +x_10 = l_Lean_replaceRef(x_1, x_9); +lean_dec(x_9); +lean_dec(x_1); +lean_ctor_set(x_5, 5, x_10); +x_11 = l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__4(x_2, x_3, x_4, x_5, x_6, x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +return x_11; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; +x_12 = lean_ctor_get(x_5, 0); +x_13 = lean_ctor_get(x_5, 1); +x_14 = lean_ctor_get(x_5, 2); +x_15 = lean_ctor_get(x_5, 3); +x_16 = lean_ctor_get(x_5, 4); +x_17 = lean_ctor_get(x_5, 5); +x_18 = lean_ctor_get(x_5, 6); +x_19 = lean_ctor_get(x_5, 7); +x_20 = lean_ctor_get(x_5, 8); +x_21 = lean_ctor_get(x_5, 9); +x_22 = lean_ctor_get(x_5, 10); +x_23 = lean_ctor_get_uint8(x_5, sizeof(void*)*11); +lean_inc(x_22); +lean_inc(x_21); +lean_inc(x_20); +lean_inc(x_19); +lean_inc(x_18); +lean_inc(x_17); +lean_inc(x_16); +lean_inc(x_15); +lean_inc(x_14); +lean_inc(x_13); +lean_inc(x_12); +lean_dec(x_5); +x_24 = l_Lean_replaceRef(x_1, x_17); +lean_dec(x_17); +lean_dec(x_1); +x_25 = lean_alloc_ctor(0, 11, 1); +lean_ctor_set(x_25, 0, x_12); +lean_ctor_set(x_25, 1, x_13); +lean_ctor_set(x_25, 2, x_14); +lean_ctor_set(x_25, 3, x_15); +lean_ctor_set(x_25, 4, x_16); +lean_ctor_set(x_25, 5, x_24); +lean_ctor_set(x_25, 6, x_18); +lean_ctor_set(x_25, 7, x_19); +lean_ctor_set(x_25, 8, x_20); +lean_ctor_set(x_25, 9, x_21); +lean_ctor_set(x_25, 10, x_22); +lean_ctor_set_uint8(x_25, sizeof(void*)*11, x_23); +x_26 = l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__4(x_2, x_3, x_4, x_25, x_6, x_7); +lean_dec(x_6); +lean_dec(x_25); +lean_dec(x_4); +lean_dec(x_3); +return x_26; +} +} +} +static lean_object* _init_l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("unknown constant '", 18); +return x_1; +} +} +static lean_object* _init_l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__1; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("'", 1); +return x_1; +} +} +static lean_object* _init_l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__3; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; +} +} +LEAN_EXPORT lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_7 = lean_box(0); +x_8 = l_Lean_Expr_const___override(x_1, x_7); +x_9 = l_Lean_MessageData_ofExpr(x_8); +x_10 = l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__2; +x_11 = lean_alloc_ctor(7, 2, 0); +lean_ctor_set(x_11, 0, x_10); +lean_ctor_set(x_11, 1, x_9); +x_12 = l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__4; +x_13 = lean_alloc_ctor(7, 2, 0); +lean_ctor_set(x_13, 0, x_11); +lean_ctor_set(x_13, 1, x_12); +x_14 = l_Lean_throwError___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___spec__3(x_13, x_2, x_3, x_4, x_5, x_6); +return x_14; +} +} +LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__5___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; lean_object* x_10; +x_9 = l_List_mapTR_loop___at_Lean_resolveGlobalConstCore___spec__2(x_1, x_2); +x_10 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_10, 0, x_9); +lean_ctor_set(x_10, 1, x_8); +return x_10; +} +} +LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; +lean_inc(x_4); +lean_inc(x_1); +x_7 = l_Lean_resolveGlobalName___at_Lean_Elab_Tactic_mkSimpOnly___spec__7(x_1, x_2, x_3, x_4, x_5, x_6); +x_8 = lean_ctor_get(x_7, 0); +lean_inc(x_8); +x_9 = lean_ctor_get(x_7, 1); +lean_inc(x_9); +lean_dec(x_7); +x_10 = lean_box(0); +x_11 = l_List_filterTR_loop___at_Lean_resolveGlobalConstCore___spec__1(x_8, x_10); +x_12 = l_List_isEmpty___rarg(x_11); +if (x_12 == 0) +{ +lean_object* x_13; lean_object* x_14; +lean_dec(x_1); +x_13 = lean_box(0); +x_14 = l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__5___lambda__1(x_11, x_10, x_13, x_2, x_3, x_4, x_5, x_9); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_14; +} +else +{ +lean_object* x_15; uint8_t x_16; +lean_dec(x_11); +x_15 = l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6(x_1, x_2, x_3, x_4, x_5, x_9); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +x_16 = !lean_is_exclusive(x_15); +if (x_16 == 0) +{ +return x_15; +} +else +{ +lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_17 = lean_ctor_get(x_15, 0); +x_18 = lean_ctor_get(x_15, 1); +lean_inc(x_18); +lean_inc(x_17); +lean_dec(x_15); +x_19 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_19, 0, x_17); +lean_ctor_set(x_19, 1, x_18); +return x_19; +} +} +} +} +static lean_object* _init_l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("expected identifier", 19); +return x_1; +} +} +static lean_object* _init_l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__1; +x_2 = lean_alloc_ctor(3, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__2; +x_2 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +LEAN_EXPORT lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +if (lean_obj_tag(x_1) == 3) +{ +lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; +x_7 = lean_ctor_get(x_1, 2); +lean_inc(x_7); +x_8 = lean_ctor_get(x_1, 3); +lean_inc(x_8); +x_9 = l_List_filterMap___at_Lean_resolveGlobalConst___spec__1(x_8); +x_10 = l_List_isEmpty___rarg(x_9); +if (x_10 == 0) +{ +lean_object* x_11; +lean_dec(x_7); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_9); +lean_ctor_set(x_11, 1, x_6); +return x_11; +} +else +{ +uint8_t x_12; +lean_dec(x_9); +x_12 = !lean_is_exclusive(x_4); +if (x_12 == 0) +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; +x_13 = lean_ctor_get(x_4, 5); +x_14 = l_Lean_replaceRef(x_1, x_13); +lean_dec(x_13); +lean_dec(x_1); +lean_ctor_set(x_4, 5, x_14); +x_15 = l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__5(x_7, x_2, x_3, x_4, x_5, x_6); +return x_15; +} +else +{ +lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; +x_16 = lean_ctor_get(x_4, 0); +x_17 = lean_ctor_get(x_4, 1); +x_18 = lean_ctor_get(x_4, 2); +x_19 = lean_ctor_get(x_4, 3); +x_20 = lean_ctor_get(x_4, 4); +x_21 = lean_ctor_get(x_4, 5); +x_22 = lean_ctor_get(x_4, 6); +x_23 = lean_ctor_get(x_4, 7); +x_24 = lean_ctor_get(x_4, 8); +x_25 = lean_ctor_get(x_4, 9); +x_26 = lean_ctor_get(x_4, 10); +x_27 = lean_ctor_get_uint8(x_4, sizeof(void*)*11); +lean_inc(x_26); +lean_inc(x_25); +lean_inc(x_24); +lean_inc(x_23); +lean_inc(x_22); +lean_inc(x_21); +lean_inc(x_20); +lean_inc(x_19); +lean_inc(x_18); +lean_inc(x_17); +lean_inc(x_16); +lean_dec(x_4); +x_28 = l_Lean_replaceRef(x_1, x_21); +lean_dec(x_21); +lean_dec(x_1); +x_29 = lean_alloc_ctor(0, 11, 1); +lean_ctor_set(x_29, 0, x_16); +lean_ctor_set(x_29, 1, x_17); +lean_ctor_set(x_29, 2, x_18); +lean_ctor_set(x_29, 3, x_19); +lean_ctor_set(x_29, 4, x_20); +lean_ctor_set(x_29, 5, x_28); +lean_ctor_set(x_29, 6, x_22); +lean_ctor_set(x_29, 7, x_23); +lean_ctor_set(x_29, 8, x_24); +lean_ctor_set(x_29, 9, x_25); +lean_ctor_set(x_29, 10, x_26); +lean_ctor_set_uint8(x_29, sizeof(void*)*11, x_27); +x_30 = l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__5(x_7, x_2, x_3, x_29, x_5, x_6); +return x_30; +} +} +} +else +{ +lean_object* x_31; lean_object* x_32; +x_31 = l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__3; +x_32 = l_Lean_throwErrorAt___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__3(x_1, x_31, x_2, x_3, x_4, x_5, x_6); +return x_32; +} +} +} +LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__8(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; lean_object* x_8; uint8_t x_9; +x_7 = lean_ctor_get(x_4, 5); +x_8 = l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(x_1, x_2, x_3, x_4, x_5, x_6); +x_9 = !lean_is_exclusive(x_8); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; +x_10 = lean_ctor_get(x_8, 0); +lean_inc(x_7); +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_7); +lean_ctor_set(x_11, 1, x_10); +lean_ctor_set_tag(x_8, 1); +lean_ctor_set(x_8, 0, x_11); +return x_8; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; +x_12 = lean_ctor_get(x_8, 0); +x_13 = lean_ctor_get(x_8, 1); +lean_inc(x_13); +lean_inc(x_12); +lean_dec(x_8); +lean_inc(x_7); +x_14 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_14, 0, x_7); +lean_ctor_set(x_14, 1, x_12); +x_15 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_15, 0, x_14); +lean_ctor_set(x_15, 1, x_13); +return x_15; +} +} +} +LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__7(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +_start: +{ +uint8_t x_8; +x_8 = !lean_is_exclusive(x_5); +if (x_8 == 0) +{ +lean_object* x_9; lean_object* x_10; lean_object* x_11; +x_9 = lean_ctor_get(x_5, 5); +x_10 = l_Lean_replaceRef(x_1, x_9); +lean_dec(x_9); +lean_dec(x_1); +lean_ctor_set(x_5, 5, x_10); +x_11 = l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__8(x_2, x_3, x_4, x_5, x_6, x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +return x_11; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; +x_12 = lean_ctor_get(x_5, 0); +x_13 = lean_ctor_get(x_5, 1); +x_14 = lean_ctor_get(x_5, 2); +x_15 = lean_ctor_get(x_5, 3); +x_16 = lean_ctor_get(x_5, 4); +x_17 = lean_ctor_get(x_5, 5); +x_18 = lean_ctor_get(x_5, 6); +x_19 = lean_ctor_get(x_5, 7); +x_20 = lean_ctor_get(x_5, 8); +x_21 = lean_ctor_get(x_5, 9); +x_22 = lean_ctor_get(x_5, 10); +x_23 = lean_ctor_get_uint8(x_5, sizeof(void*)*11); +lean_inc(x_22); +lean_inc(x_21); +lean_inc(x_20); +lean_inc(x_19); +lean_inc(x_18); +lean_inc(x_17); +lean_inc(x_16); +lean_inc(x_15); +lean_inc(x_14); +lean_inc(x_13); +lean_inc(x_12); +lean_dec(x_5); +x_24 = l_Lean_replaceRef(x_1, x_17); +lean_dec(x_17); +lean_dec(x_1); +x_25 = lean_alloc_ctor(0, 11, 1); +lean_ctor_set(x_25, 0, x_12); +lean_ctor_set(x_25, 1, x_13); +lean_ctor_set(x_25, 2, x_14); +lean_ctor_set(x_25, 3, x_15); +lean_ctor_set(x_25, 4, x_16); +lean_ctor_set(x_25, 5, x_24); +lean_ctor_set(x_25, 6, x_18); +lean_ctor_set(x_25, 7, x_19); +lean_ctor_set(x_25, 8, x_20); +lean_ctor_set(x_25, 9, x_21); +lean_ctor_set(x_25, 10, x_22); +lean_ctor_set_uint8(x_25, sizeof(void*)*11, x_23); +x_26 = l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__8(x_2, x_3, x_4, x_25, x_6, x_7); +lean_dec(x_6); +lean_dec(x_25); +lean_dec(x_4); +lean_dec(x_3); +return x_26; +} +} +} +static lean_object* _init_l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("ambiguous identifier '", 22); +return x_1; +} +} +static lean_object* _init_l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__2() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("', possible interpretations: ", 29); +return x_1; +} +} +LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +lean_inc(x_5); +lean_inc(x_4); +lean_inc(x_3); +lean_inc(x_2); +lean_inc(x_1); +x_7 = l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2(x_1, x_2, x_3, x_4, x_5, x_6); +if (lean_obj_tag(x_7) == 0) +{ +lean_object* x_8; +x_8 = lean_ctor_get(x_7, 0); +lean_inc(x_8); +if (lean_obj_tag(x_8) == 0) +{ +lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; +x_9 = lean_ctor_get(x_7, 1); +lean_inc(x_9); +lean_dec(x_7); +x_10 = lean_box(0); +x_11 = 0; +x_12 = lean_unsigned_to_nat(0u); +lean_inc(x_1); +x_13 = l_Lean_Syntax_formatStxAux(x_10, x_11, x_12, x_1); +x_14 = l_Std_Format_defWidth; +x_15 = lean_format_pretty(x_13, x_14, x_12, x_12); +x_16 = l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__1; +x_17 = lean_string_append(x_16, x_15); +lean_dec(x_15); +x_18 = l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__2; +x_19 = lean_string_append(x_17, x_18); +x_20 = lean_box(0); +x_21 = l_List_mapTR_loop___at_Lean_resolveGlobalConstNoOverload___spec__1(x_8, x_20); +x_22 = l_List_toString___at_Lean_resolveGlobalConstNoOverloadCore___spec__2(x_21); +lean_dec(x_21); +x_23 = lean_string_append(x_19, x_22); +lean_dec(x_22); +x_24 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__3___closed__6; +x_25 = lean_string_append(x_23, x_24); +x_26 = lean_alloc_ctor(3, 1, 0); +lean_ctor_set(x_26, 0, x_25); +x_27 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_27, 0, x_26); +x_28 = l_Lean_throwErrorAt___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__7(x_1, x_27, x_2, x_3, x_4, x_5, x_9); +return x_28; +} +else +{ +lean_object* x_29; +x_29 = lean_ctor_get(x_8, 1); +lean_inc(x_29); +if (lean_obj_tag(x_29) == 0) +{ +uint8_t x_30; +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_30 = !lean_is_exclusive(x_7); +if (x_30 == 0) +{ +lean_object* x_31; lean_object* x_32; +x_31 = lean_ctor_get(x_7, 0); +lean_dec(x_31); +x_32 = lean_ctor_get(x_8, 0); +lean_inc(x_32); +lean_dec(x_8); +lean_ctor_set(x_7, 0, x_32); +return x_7; +} +else +{ +lean_object* x_33; lean_object* x_34; lean_object* x_35; +x_33 = lean_ctor_get(x_7, 1); +lean_inc(x_33); +lean_dec(x_7); +x_34 = lean_ctor_get(x_8, 0); +lean_inc(x_34); +lean_dec(x_8); +x_35 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_35, 0, x_34); +lean_ctor_set(x_35, 1, x_33); +return x_35; +} +} +else +{ +lean_object* x_36; lean_object* x_37; uint8_t x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; +lean_dec(x_29); +x_36 = lean_ctor_get(x_7, 1); +lean_inc(x_36); +lean_dec(x_7); +x_37 = lean_box(0); +x_38 = 0; +x_39 = lean_unsigned_to_nat(0u); +lean_inc(x_1); +x_40 = l_Lean_Syntax_formatStxAux(x_37, x_38, x_39, x_1); +x_41 = l_Std_Format_defWidth; +x_42 = lean_format_pretty(x_40, x_41, x_39, x_39); +x_43 = l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__1; +x_44 = lean_string_append(x_43, x_42); +lean_dec(x_42); +x_45 = l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__2; +x_46 = lean_string_append(x_44, x_45); +x_47 = lean_box(0); +x_48 = l_List_mapTR_loop___at_Lean_resolveGlobalConstNoOverload___spec__1(x_8, x_47); +x_49 = l_List_toString___at_Lean_resolveGlobalConstNoOverloadCore___spec__2(x_48); +lean_dec(x_48); +x_50 = lean_string_append(x_46, x_49); +lean_dec(x_49); +x_51 = l_Lean_withTraceNode___at_Lean_Elab_Tactic_NormCast_proveEqUsingDown___spec__1___lambda__3___closed__6; +x_52 = lean_string_append(x_50, x_51); +x_53 = lean_alloc_ctor(3, 1, 0); +lean_ctor_set(x_53, 0, x_52); +x_54 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_54, 0, x_53); +x_55 = l_Lean_throwErrorAt___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__7(x_1, x_54, x_2, x_3, x_4, x_5, x_36); +return x_55; +} +} +} +else +{ +uint8_t x_56; +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_56 = !lean_is_exclusive(x_7); +if (x_56 == 0) +{ +return x_7; +} +else +{ +lean_object* x_57; lean_object* x_58; lean_object* x_59; +x_57 = lean_ctor_get(x_7, 0); +x_58 = lean_ctor_get(x_7, 1); +lean_inc(x_58); +lean_inc(x_57); +lean_dec(x_7); +x_59 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_59, 0, x_57); +lean_ctor_set(x_59, 1, x_58); +return x_59; +} +} +} +} +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +lean_inc(x_5); +lean_inc(x_4); +lean_inc(x_3); +lean_inc(x_2); +x_7 = l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1(x_1, x_2, x_3, x_4, x_5, x_6); +if (lean_obj_tag(x_7) == 0) +{ +lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; +x_8 = lean_ctor_get(x_7, 0); +lean_inc(x_8); +x_9 = lean_ctor_get(x_7, 1); +lean_inc(x_9); +lean_dec(x_7); +x_10 = 0; +x_11 = lean_unsigned_to_nat(1000u); +x_12 = l_Lean_Meta_NormCast_addElim(x_8, x_10, x_11, x_2, x_3, x_4, x_5, x_9); +return x_12; +} +else +{ +uint8_t x_13; +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +x_13 = !lean_is_exclusive(x_7); +if (x_13 == 0) +{ +return x_7; +} +else +{ +lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_14 = lean_ctor_get(x_7, 0); +x_15 = lean_ctor_get(x_7, 1); +lean_inc(x_15); +lean_inc(x_14); +lean_dec(x_7); +x_16 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_16, 0, x_14); +lean_ctor_set(x_16, 1, x_15); +return x_16; +} +} +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("normCastAddElim", 15); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_1 = l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__4; +x_2 = l_Lean_Elab_Tactic_NormCast_evalNormCast0___closed__1; +x_3 = l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__1; +x_4 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1; +x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4); +return x_5; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("ident", 5); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3; +x_3 = l_Lean_Name_str___override(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__5() { +_start: +{ +uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5; +x_1 = 0; +x_2 = 1; +x_3 = 1; +x_4 = 0; +x_5 = lean_alloc_ctor(0, 0, 12); +lean_ctor_set_uint8(x_5, 0, x_1); +lean_ctor_set_uint8(x_5, 1, x_1); +lean_ctor_set_uint8(x_5, 2, x_1); +lean_ctor_set_uint8(x_5, 3, x_1); +lean_ctor_set_uint8(x_5, 4, x_1); +lean_ctor_set_uint8(x_5, 5, x_2); +lean_ctor_set_uint8(x_5, 6, x_2); +lean_ctor_set_uint8(x_5, 7, x_1); +lean_ctor_set_uint8(x_5, 8, x_2); +lean_ctor_set_uint8(x_5, 9, x_3); +lean_ctor_set_uint8(x_5, 10, x_1); +lean_ctor_set_uint8(x_5, 11, x_4); +return x_5; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__6() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_box(0), lean_box(0)); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__6; +x_2 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7; +x_2 = lean_unsigned_to_nat(0u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__9() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(32u); +x_2 = lean_mk_empty_array_with_capacity(x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__10() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__9; +x_2 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__11() { +_start: +{ +size_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_1 = 5; +x_2 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__10; +x_3 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__9; +x_4 = lean_unsigned_to_nat(0u); +x_5 = lean_alloc_ctor(0, 4, sizeof(size_t)*1); +lean_ctor_set(x_5, 0, x_2); +lean_ctor_set(x_5, 1, x_3); +lean_ctor_set(x_5, 2, x_4); +lean_ctor_set(x_5, 3, x_4); +lean_ctor_set_usize(x_5, 4, x_1); +return x_5; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__12() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__8; +x_2 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__11; +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__13() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__5; +x_3 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__12; +x_4 = l_Lean_Elab_Tactic_NormCast_derive___lambda__11___closed__2; +x_5 = lean_unsigned_to_nat(0u); +x_6 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_6, 0, x_2); +lean_ctor_set(x_6, 1, x_3); +lean_ctor_set(x_6, 2, x_4); +lean_ctor_set(x_6, 3, x_1); +lean_ctor_set(x_6, 4, x_5); +lean_ctor_set(x_6, 5, x_1); +return x_6; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__14() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7; +x_2 = lean_unsigned_to_nat(0u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__15() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7; +x_2 = lean_unsigned_to_nat(0u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__16() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7; +x_2 = lean_unsigned_to_nat(0u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__17() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_1 = lean_unsigned_to_nat(0u); +x_2 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__14; +x_3 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__15; +x_4 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__16; +x_5 = lean_alloc_ctor(0, 9, 0); +lean_ctor_set(x_5, 0, x_1); +lean_ctor_set(x_5, 1, x_1); +lean_ctor_set(x_5, 2, x_1); +lean_ctor_set(x_5, 3, x_2); +lean_ctor_set(x_5, 4, x_3); +lean_ctor_set(x_5, 5, x_4); +lean_ctor_set(x_5, 6, x_2); +lean_ctor_set(x_5, 7, x_3); +lean_ctor_set(x_5, 8, x_3); +return x_5; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__18() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7; +x_2 = lean_unsigned_to_nat(0u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__19() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_instHashableInfoCacheKey___boxed), 1, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__20() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7; +x_2 = lean_unsigned_to_nat(0u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__21() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_instBEqLocalInstance___boxed), 2, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__22() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__21; +x_2 = lean_alloc_closure((void*)(l_Array_instBEqArray___rarg___boxed), 3, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__23() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__22; +x_2 = l_Lean_Expr_instBEqExpr; +x_3 = lean_alloc_closure((void*)(l_instBEqProd___rarg), 4, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__24() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_instHashableLocalInstance___boxed), 1, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__25() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__24; +x_2 = lean_alloc_closure((void*)(l_instHashableArray___rarg___boxed), 2, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__26() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__25; +x_2 = l_Lean_Expr_instHashableExpr; +x_3 = lean_alloc_closure((void*)(l_instHashableProd___rarg___boxed), 3, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__27() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7; +x_2 = lean_unsigned_to_nat(0u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__28() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Expr_instBEqExpr; +x_2 = lean_alloc_closure((void*)(l_instBEqProd___rarg), 4, 2); +lean_closure_set(x_2, 0, x_1); +lean_closure_set(x_2, 1, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__29() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Expr_instHashableExpr; +x_2 = lean_alloc_closure((void*)(l_instHashableProd___rarg___boxed), 3, 2); +lean_closure_set(x_2, 0, x_1); +lean_closure_set(x_2, 1, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__30() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7; +x_2 = lean_unsigned_to_nat(0u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__31() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__30; +x_2 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_2, 0, x_1); +lean_ctor_set(x_2, 1, x_1); +lean_ctor_set(x_2, 2, x_1); +lean_ctor_set(x_2, 3, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__32() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_1 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__18; +x_2 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__20; +x_3 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__27; +x_4 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__31; +x_5 = lean_alloc_ctor(0, 7, 0); +lean_ctor_set(x_5, 0, x_1); +lean_ctor_set(x_5, 1, x_2); +lean_ctor_set(x_5, 2, x_3); +lean_ctor_set(x_5, 3, x_1); +lean_ctor_set(x_5, 4, x_1); +lean_ctor_set(x_5, 5, x_4); +lean_ctor_set(x_5, 6, x_4); +return x_5; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__33() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__17; +x_3 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__32; +x_4 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__11; +x_5 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_5, 0, x_2); +lean_ctor_set(x_5, 1, x_3); +lean_ctor_set(x_5, 2, x_1); +lean_ctor_set(x_5, 3, x_4); +return x_5; +} +} +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; uint8_t x_6; +x_5 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2; +lean_inc(x_1); +x_6 = l_Lean_Syntax_isOfKind(x_1, x_5); +if (x_6 == 0) +{ +lean_object* x_7; +lean_dec(x_1); +x_7 = l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabAuxDef___spec__1___rarg(x_4); +return x_7; +} +else +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; +x_8 = lean_unsigned_to_nat(1u); +x_9 = l_Lean_Syntax_getArg(x_1, x_8); +lean_dec(x_1); +x_10 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4; +lean_inc(x_9); +x_11 = l_Lean_Syntax_isOfKind(x_9, x_10); +if (x_11 == 0) +{ +lean_object* x_12; +lean_dec(x_9); +x_12 = l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabAuxDef___spec__1___rarg(x_4); +return x_12; +} +else +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; +x_13 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_NormCast_elabAddElim___lambda__1), 6, 1); +lean_closure_set(x_13, 0, x_9); +x_14 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__13; +x_15 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__33; +x_16 = lean_alloc_closure((void*)(l_Lean_Meta_MetaM_run_x27___rarg), 6, 3); +lean_closure_set(x_16, 0, x_13); +lean_closure_set(x_16, 1, x_14); +lean_closure_set(x_16, 2, x_15); +x_17 = l_Lean_Elab_Command_liftCoreM___rarg(x_16, x_2, x_3, x_4); +return x_17; +} +} +} +} +LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__4(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_7; +} +} +LEAN_EXPORT lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_7; +} +} +LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__5___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; +x_9 = l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__5___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +return x_9; +} +} +LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__8___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = l_Lean_throwError___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__8(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_7; +} +} +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_NormCast_elabAddElim___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = l_Lean_Elab_Tactic_NormCast_elabAddElim(x_1, x_2, x_3, x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_5; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("elabAddElim", 11); +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_1 = l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__4; +x_2 = l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__6; +x_3 = l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__1; +x_4 = l_Lean_Elab_Tactic_NormCast_initFn____x40_Lean_Elab_Tactic_NormCast___hyg_6____closed__9; +x_5 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1; +x_6 = l_Lean_Name_mkStr5(x_1, x_2, x_3, x_4, x_5); +return x_6; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Elab_Command_commandElabAttribute; +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_NormCast_elabAddElim___boxed), 4, 0); +return x_1; +} +} +LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_2 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3; +x_3 = l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2; +x_4 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2; +x_5 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4; +x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1); +return x_6; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_unsigned_to_nat(266u); +x_2 = lean_unsigned_to_nat(54u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_unsigned_to_nat(271u); +x_2 = lean_unsigned_to_nat(31u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_1 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__1; +x_2 = lean_unsigned_to_nat(54u); +x_3 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__2; +x_4 = lean_unsigned_to_nat(31u); +x_5 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_5, 0, x_1); +lean_ctor_set(x_5, 1, x_2); +lean_ctor_set(x_5, 2, x_3); +lean_ctor_set(x_5, 3, x_4); +return x_5; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_unsigned_to_nat(266u); +x_2 = lean_unsigned_to_nat(58u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_unsigned_to_nat(266u); +x_2 = lean_unsigned_to_nat(69u); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_1 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__4; +x_2 = lean_unsigned_to_nat(58u); +x_3 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__5; +x_4 = lean_unsigned_to_nat(69u); +x_5 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_5, 0, x_1); +lean_ctor_set(x_5, 1, x_2); +lean_ctor_set(x_5, 2, x_3); +lean_ctor_set(x_5, 3, x_4); +return x_5; +} +} +static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__3; +x_2 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__6; +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_2 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2; +x_3 = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__7; +x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1); +return x_4; +} +} lean_object* initialize_Init(uint8_t builtin, lean_object*); lean_object* initialize_Lean_Meta_Tactic_NormCast(uint8_t builtin, lean_object*); lean_object* initialize_Lean_Elab_Tactic_Conv_Simp(uint8_t builtin, lean_object*); @@ -15710,6 +17154,118 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast_declR if (builtin) {res = l___regBuiltin_Lean_Elab_Tactic_NormCast_evalPushCast_declRange(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +}l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__1 = _init_l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__1(); +lean_mark_persistent(l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__1); +l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__2 = _init_l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__2(); +lean_mark_persistent(l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__2); +l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__3 = _init_l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__3(); +lean_mark_persistent(l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__3); +l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__4 = _init_l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__4(); +lean_mark_persistent(l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__6___closed__4); +l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__1 = _init_l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__1(); +lean_mark_persistent(l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__1); +l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__2 = _init_l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__2(); +lean_mark_persistent(l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__2); +l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__3 = _init_l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__3(); +lean_mark_persistent(l_Lean_resolveGlobalConst___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__2___closed__3); +l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__1 = _init_l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__1(); +lean_mark_persistent(l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__1); +l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__2 = _init_l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__2(); +lean_mark_persistent(l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Tactic_NormCast_elabAddElim___spec__1___closed__2); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__5 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__5(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__5); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__6 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__6(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__6); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__7); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__8 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__8(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__8); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__9 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__9(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__9); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__10 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__10(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__10); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__11 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__11(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__11); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__12 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__12(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__12); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__13 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__13(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__13); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__14 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__14(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__14); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__15 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__15(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__15); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__16 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__16(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__16); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__17 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__17(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__17); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__18 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__18(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__18); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__19 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__19(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__19); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__20 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__20(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__20); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__21 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__21(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__21); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__22 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__22(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__22); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__23 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__23(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__23); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__24 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__24(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__24); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__25 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__25(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__25); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__26 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__26(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__26); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__27 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__27(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__27); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__28 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__28(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__28); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__29 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__29(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__29); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__30 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__30(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__30); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__31 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__31(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__31); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__32 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__32(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__32); +l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__33 = _init_l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__33(); +lean_mark_persistent(l_Lean_Elab_Tactic_NormCast_elabAddElim___closed__33); +l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__1); +l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__2); +l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__3); +l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim___closed__4); +if (builtin) {res = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +}l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__1); +l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__2(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__2); +l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__3(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__3); +l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__4 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__4(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__4); +l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__5 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__5(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__5); +l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__6 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__6(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__6); +l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__7 = _init_l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__7(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange___closed__7); +if (builtin) {res = l___regBuiltin_Lean_Elab_Tactic_NormCast_elabAddElim_declRange(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); }return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Lean/Meta/Tactic/NormCast.c b/stage0/stdlib/Lean/Meta/Tactic/NormCast.c index 75ed8e234c..aeb067e51b 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/NormCast.c +++ b/stage0/stdlib/Lean/Meta/Tactic/NormCast.c @@ -5677,12 +5677,12 @@ l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586____close lean_mark_persistent(l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586____closed__7); l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586____closed__8 = _init_l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586____closed__8(); lean_mark_persistent(l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586____closed__8); -res = l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586_(lean_io_mk_world()); +if (builtin) {res = l_Lean_Meta_NormCast_initFn____x40_Lean_Meta_Tactic_NormCast___hyg_1586_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Meta_NormCast_pushCastExt = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Meta_NormCast_pushCastExt); lean_dec_ref(res); -l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__1 = _init_l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__1(); +}l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__1 = _init_l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__1(); l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__2 = _init_l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__2(); lean_mark_persistent(l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__1___closed__2); l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__3___closed__1 = _init_l_Lean_Meta_NormCast_instInhabitedNormCastExtension___lambda__3___closed__1(); diff --git a/stage0/stdlib/Lean/Meta/Tactic/TryThis.c b/stage0/stdlib/Lean/Meta/Tactic/TryThis.c index b79155c857..7dea181ed1 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/TryThis.c +++ b/stage0/stdlib/Lean/Meta/Tactic/TryThis.c @@ -91,6 +91,7 @@ lean_object* l_Lean_Elab_pushInfoLeaf___at_Lean_Widget_savePanelWidgetInfo___spe static lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___spec__1___closed__6; static lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___spec__1___closed__7; static lean_object* l_Lean_Meta_Tactic_TryThis_SuggestionStyle_asHypothesis___closed__2; +static lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2; static lean_object* l_Std_Range_forIn_x27_loop___at_Lean_Meta_Tactic_TryThis_tryThisProvider___spec__1___closed__3; static lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisWidget___closed__4; lean_object* l_Lean_logAt___at_Lean_Meta_computeSynthOrder___spec__7(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -143,6 +144,7 @@ static lean_object* l_Lean_Meta_Tactic_TryThis_addHaveSuggestion___closed__3; lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonCommand____x40_Lean_Data_Lsp_Basic___hyg_1545____spec__2(size_t, size_t, lean_object*); static lean_object* l_Lean_Meta_Tactic_TryThis_instInhabitedSuggestionText___closed__1; static lean_object* l_Lean_Meta_Tactic_TryThis_SuggestionStyle_value___closed__8; +static lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Tactic_TryThis_addExactSuggestions___spec__1(uint8_t, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Meta_Tactic_TryThis_getInputWidth___closed__1; LEAN_EXPORT lean_object* l_Lean_Syntax_replaceM___at_Lean_Meta_Tactic_TryThis_delabToRefinableSyntax___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -250,6 +252,7 @@ lean_object* l_Lean_Syntax_node2(lean_object*, lean_object*, lean_object*, lean_ static lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_Tactic_TryThis_addSuggestions___spec__2___closed__1; static lean_object* l_Lean_Syntax_replaceM___at_Lean_Meta_Tactic_TryThis_replaceMVarsByUnderscores___spec__1___rarg___lambda__3___closed__4; lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*); +lean_object* l_Lean_Server_addBuiltinCodeActionProvider(lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Meta_Tactic_TryThis_0__Lean_Meta_Tactic_TryThis_addExactSuggestionCore___closed__4; static lean_object* l_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___closed__11; static lean_object* l_Lean_Meta_Tactic_TryThis_addHaveSuggestion___closed__36; @@ -258,6 +261,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Tactic_TryThis_addExactSuggestion___boxed(l LEAN_EXPORT lean_object* l_Lean_Meta_Tactic_TryThis_Suggestion_toCodeActionTitle_x3f___default; static lean_object* l_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___closed__10; static lean_object* l_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___lambda__2___closed__5; +static lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3; LEAN_EXPORT lean_object* l_Lean_Meta_Tactic_TryThis_SuggestionStyle_warning___boxed(lean_object*); static lean_object* l_Lean_Meta_Tactic_TryThis_addHaveSuggestion___closed__44; LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Meta_Tactic_TryThis_addSuggestions___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -442,6 +446,7 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*); static lean_object* l_Lean_Meta_Tactic_TryThis_SuggestionStyle_warning___closed__14; uint8_t lean_usize_dec_lt(size_t, size_t); static lean_object* l_Lean_Meta_Tactic_TryThis_SuggestionStyle_warning___closed__2; +LEAN_EXPORT lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider(lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Tactic_TryThis_replaceMVarsByUnderscores___spec__2___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_Tactic_TryThis_addRewriteSuggestion___spec__1___closed__2; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Tactic_TryThis_0__Lean_Meta_Tactic_TryThis_addSuggestionCore___spec__2___boxed(lean_object*, lean_object*, lean_object*); @@ -1191,6 +1196,45 @@ lean_dec(x_3); return x_5; } } +static lean_object* _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("tryThisProvider", 15); +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_1 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisWidget___closed__1; +x_2 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisWidget___closed__2; +x_3 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisWidget___closed__3; +x_4 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisWidget___closed__4; +x_5 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1; +x_6 = l_Lean_Name_mkStr5(x_1, x_2, x_3, x_4, x_5); +return x_6; +} +} +static lean_object* _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Meta_Tactic_TryThis_tryThisProvider___boxed), 4, 0); +return x_1; +} +} +LEAN_EXPORT lean_object* l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_2 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2; +x_3 = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3; +x_4 = l_Lean_Server_addBuiltinCodeActionProvider(x_2, x_3, x_1); +return x_4; +} +} LEAN_EXPORT uint8_t l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___lambda__1(uint32_t x_1) { _start: { @@ -9391,7 +9435,16 @@ l_Std_Range_forIn_x27_loop___at_Lean_Meta_Tactic_TryThis_tryThisProvider___spec_ lean_mark_persistent(l_Std_Range_forIn_x27_loop___at_Lean_Meta_Tactic_TryThis_tryThisProvider___spec__1___closed__4); l_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1 = _init_l_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1(); lean_mark_persistent(l_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1); -l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___closed__1 = _init_l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___closed__1(); +l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1 = _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__1); +l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2 = _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2(); +lean_mark_persistent(l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__2); +l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3 = _init_l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3(); +lean_mark_persistent(l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider___closed__3); +if (builtin) {res = l___regBuiltin_Lean_Meta_Tactic_TryThis_tryThisProvider(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +}l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___closed__1 = _init_l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___closed__1(); lean_mark_persistent(l_Lean_Meta_Tactic_TryThis_getIndentAndColumn___closed__1); l_Lean_Syntax_replaceM___at_Lean_Meta_Tactic_TryThis_replaceMVarsByUnderscores___spec__1___rarg___lambda__3___closed__1 = _init_l_Lean_Syntax_replaceM___at_Lean_Meta_Tactic_TryThis_replaceMVarsByUnderscores___spec__1___rarg___lambda__3___closed__1(); lean_mark_persistent(l_Lean_Syntax_replaceM___at_Lean_Meta_Tactic_TryThis_replaceMVarsByUnderscores___spec__1___rarg___lambda__3___closed__1);