From 689acab1d3490913f353c32fdffc05e9d7a26fdf Mon Sep 17 00:00:00 2001 From: Lean stage0 autoupdater <> Date: Mon, 14 Apr 2025 07:03:16 +0000 Subject: [PATCH] chore: update stage0 --- stage0/stdlib/Init/Data/List/Perm.c | 6 +- stage0/stdlib/Init/Grind.c | 6 +- stage0/stdlib/Init/Grind/Ext.c | 33 + stage0/stdlib/Init/Meta.c | 2 +- .../stdlib/Lean/Elab/Tactic/BuiltinTactic.c | 1515 ++++++++--------- stage0/stdlib/Lean/Elab/Tactic/Induction.c | 940 ++++++---- .../stdlib/Lean/Meta/Tactic/Grind/ExtAttr.c | 2 +- 7 files changed, 1391 insertions(+), 1113 deletions(-) create mode 100644 stage0/stdlib/Init/Grind/Ext.c diff --git a/stage0/stdlib/Init/Data/List/Perm.c b/stage0/stdlib/Init/Data/List/Perm.c index fc00b33acb..3c6df9d360 100644 --- a/stage0/stdlib/Init/Data/List/Perm.c +++ b/stage0/stdlib/Init/Data/List/Perm.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Init.Data.List.Perm -// Imports: Init.Data.List.Pairwise Init.Data.List.Erase +// Imports: Init.Data.List.Pairwise Init.Data.List.Erase Init.Data.List.Find #include #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -348,6 +348,7 @@ return x_5; } lean_object* initialize_Init_Data_List_Pairwise(uint8_t builtin, lean_object*); lean_object* initialize_Init_Data_List_Erase(uint8_t builtin, lean_object*); +lean_object* initialize_Init_Data_List_Find(uint8_t builtin, lean_object*); static bool _G_initialized = false; LEAN_EXPORT lean_object* initialize_Init_Data_List_Perm(uint8_t builtin, lean_object* w) { lean_object * res; @@ -359,6 +360,9 @@ lean_dec_ref(res); res = initialize_Init_Data_List_Erase(builtin, lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Init_Data_List_Find(builtin, lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Init/Grind.c b/stage0/stdlib/Init/Grind.c index 1fcf93abde..33e69b3c38 100644 --- a/stage0/stdlib/Init/Grind.c +++ b/stage0/stdlib/Init/Grind.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Init.Grind -// Imports: Init.Grind.Norm Init.Grind.Tactics Init.Grind.Lemmas Init.Grind.Cases Init.Grind.Propagator Init.Grind.Util Init.Grind.Offset Init.Grind.PP Init.Grind.CommRing +// Imports: Init.Grind.Norm Init.Grind.Tactics Init.Grind.Lemmas Init.Grind.Cases Init.Grind.Propagator Init.Grind.Util Init.Grind.Offset Init.Grind.PP Init.Grind.CommRing Init.Grind.Ext #include #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -22,6 +22,7 @@ lean_object* initialize_Init_Grind_Util(uint8_t builtin, lean_object*); lean_object* initialize_Init_Grind_Offset(uint8_t builtin, lean_object*); lean_object* initialize_Init_Grind_PP(uint8_t builtin, lean_object*); lean_object* initialize_Init_Grind_CommRing(uint8_t builtin, lean_object*); +lean_object* initialize_Init_Grind_Ext(uint8_t builtin, lean_object*); static bool _G_initialized = false; LEAN_EXPORT lean_object* initialize_Init_Grind(uint8_t builtin, lean_object* w) { lean_object * res; @@ -54,6 +55,9 @@ lean_dec_ref(res); res = initialize_Init_Grind_CommRing(builtin, lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Init_Grind_Ext(builtin, lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Init/Grind/Ext.c b/stage0/stdlib/Init/Grind/Ext.c new file mode 100644 index 0000000000..b0f7324370 --- /dev/null +++ b/stage0/stdlib/Init/Grind/Ext.c @@ -0,0 +1,33 @@ +// Lean compiler output +// Module: Init.Grind.Ext +// Imports: Init.Ext Init.Grind.Tactics +#include +#if defined(__clang__) +#pragma clang diagnostic ignored "-Wunused-parameter" +#pragma clang diagnostic ignored "-Wunused-label" +#elif defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wunused-parameter" +#pragma GCC diagnostic ignored "-Wunused-label" +#pragma GCC diagnostic ignored "-Wunused-but-set-variable" +#endif +#ifdef __cplusplus +extern "C" { +#endif +lean_object* initialize_Init_Ext(uint8_t builtin, lean_object*); +lean_object* initialize_Init_Grind_Tactics(uint8_t builtin, lean_object*); +static bool _G_initialized = false; +LEAN_EXPORT lean_object* initialize_Init_Grind_Ext(uint8_t builtin, lean_object* w) { +lean_object * res; +if (_G_initialized) return lean_io_result_mk_ok(lean_box(0)); +_G_initialized = true; +res = initialize_Init_Ext(builtin, lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +res = initialize_Init_Grind_Tactics(builtin, lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +return lean_io_result_mk_ok(lean_box(0)); +} +#ifdef __cplusplus +} +#endif diff --git a/stage0/stdlib/Init/Meta.c b/stage0/stdlib/Init/Meta.c index f156b88912..0be5a4478d 100644 --- a/stage0/stdlib/Init/Meta.c +++ b/stage0/stdlib/Init/Meta.c @@ -14851,7 +14851,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l_List_foldr___at_Substring_toName___spec__1___closed__1; x_2 = l_List_foldr___at_Substring_toName___spec__1___closed__2; -x_3 = lean_unsigned_to_nat(1031u); +x_3 = lean_unsigned_to_nat(1039u); x_4 = lean_unsigned_to_nat(10u); x_5 = l_List_foldr___at_Substring_toName___spec__1___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); diff --git a/stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c b/stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c index ee70a8bdab..e4c70389f6 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c +++ b/stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c @@ -39,7 +39,6 @@ static lean_object* l_Lean_Elab_Tactic_evalIntro___closed__26; static lean_object* l_Lean_Elab_Tactic_evalRunTac___closed__12; static lean_object* l_Lean_resolveNamespace___at_Lean_Elab_Tactic_evalOpen___spec__6___closed__1; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalLeft__1___closed__3; -LEAN_EXPORT lean_object* l_List_forM___at_Lean_Elab_Tactic_evalAllGoals___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRotateLeft_declRange__1___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_withRestoreOrSaveFull___at_Lean_Elab_Tactic_evalSepTactics_goEven___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_resolveNamespaceCore___at_Lean_Elab_Tactic_evalOpen___spec__9(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -189,6 +188,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_forEachVar___boxed(lean_object*, lea static lean_object* l_Lean_Elab_Tactic_evalIntro___closed__33; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRight__1___closed__1; static lean_object* l_Lean_Elab_Tactic_evalRunTac___closed__1; +lean_object* l_Lean_Core_getMessageLog___rarg(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_evalLeft___rarg___lambda__1___closed__2; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSubst__1___closed__1; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq1_declRange__1___closed__1; @@ -251,6 +251,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalSubstEqs___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalIntro_introStep(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___at_Lean_Elab_Tactic_evalOpen___spec__35(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_evalIntro___closed__17; +LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTraceState_declRange__1___closed__5; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSleep__1___closed__2; LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAssumption_declRange__1(lean_object*); @@ -841,6 +842,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq_declRange__1__ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalWithAnnotateState__1___closed__2; uint8_t l_Lean_Syntax_matchesNull(lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq_declRange__1___closed__7; +lean_object* l_Lean_Core_setMessageLog(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAnyGoals__1___closed__5; lean_object* l_Lean_MVarId_assumption(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_addOpenDecl___at_Lean_Elab_Tactic_evalOpen___spec__24(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -972,9 +974,11 @@ LEAN_EXPORT lean_object* l_Lean_addRawTrace___at_Lean_Elab_Tactic_evalTraceState LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRefl__1(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_withRestoreOrSaveFull___at_Lean_Elab_Tactic_evalSepTactics_goEven___spec__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_EXPORT lean_object* l_Lean_Elab_Tactic_forEachVar(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_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg(lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalOpen___spec__10(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_evalContradiction___rarg___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_introNCore(lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__2; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalFirst_loop(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_evalFirst__1___closed__5; static lean_object* l_Lean_Elab_Tactic_evalReplace___closed__3; @@ -1017,7 +1021,6 @@ lean_object* l_Lean_Elab_Term_addLocalVarInfo(lean_object*, lean_object*, lean_o static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRotateRight_declRange__1___closed__3; static lean_object* l_Lean_Elab_Tactic_evalRunTac___closed__6; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalLeft_declRange__1___closed__3; -LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___at_Lean_Elab_Tactic_evalOpen___spec__35___closed__4; static lean_object* l_Lean_Elab_Tactic_evalIntro___closed__8; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq1__1___closed__3; @@ -1046,7 +1049,6 @@ static lean_object* l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Tactic_eval LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalIntro_introStep___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*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalUnknown_declRange__1___closed__3; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAllGoals_declRange__1___closed__7; -LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_app___override(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_BuiltinTactic_0__Lean_Elab_Tactic_getCaseGoals_commaList(lean_object*); LEAN_EXPORT lean_object* l_Lean_filterFieldList___at_Lean_Elab_Tactic_evalOpen___spec__16___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*); @@ -1069,13 +1071,13 @@ LEAN_EXPORT lean_object* l_Lean_PersistentArray_mapM___at_Lean_Elab_Tactic_renam static lean_object* l_Lean_Elab_withSaveInfoContext___at_Lean_Elab_Tactic_renameInaccessibles___spec__3___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalDone___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_evalReplace___closed__2; -LEAN_EXPORT lean_object* l_List_forM___at_Lean_Elab_Tactic_evalAllGoals___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRight_declRange__1___closed__6; lean_object* l_Lean_Language_SnapshotTask_cancelRec___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSkip__1(lean_object*); static lean_object* l___private_Lean_Elab_Tactic_BuiltinTactic_0__Lean_Elab_Tactic_getCaseGoals_notFound___closed__4; LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_evalIntro___closed__11; +LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTraceMessage_declRange__1___closed__2; uint8_t lean_nat_dec_lt(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalRotateLeft___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1231,7 +1233,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalParen__1___closed__5; LEAN_EXPORT lean_object* l_Lean_ensureNoOverload___at_Lean_Elab_Tactic_evalOpen___spec__20___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_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*); lean_object* l_Array_ofSubarray___rarg(lean_object*); -static lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__1; LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at___private_Lean_Elab_Tactic_BuiltinTactic_0__Lean_Elab_Tactic_getCaseGoals___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRight_declRange__1___closed__1; LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1302,7 +1303,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalWithAnnotateState_declRa static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFirst__1___closed__3; static lean_object* l_Lean_Elab_Tactic_evalSepTactics_goEven___lambda__5___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalIntros___lambda__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_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg(lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalWithAnnotateState__1___closed__5; LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_elabSetOption_declRange__1(lean_object*); static lean_object* l_Lean_Elab_Tactic_elabSetOption___closed__1; @@ -1351,7 +1351,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDone_declRange__1___clos LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalOpen___spec__19___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalRotateLeft(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_evalSubstEqs___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_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__2; lean_object* l_Lean_Meta_sortFVarIds(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalFail(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_evalTactic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1404,6 +1403,7 @@ static lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAllGoals_declRange__1___closed__1; LEAN_EXPORT lean_object* l_Lean_Meta_withRestoreOrSaveFull___at_Lean_Elab_Tactic_evalSepTactics_goEven___spec__11(lean_object*, 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_Lean_Elab_unsupportedSyntaxExceptionId; +static lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__1; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalLeft_declRange__1___closed__6; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRotateRight_declRange__1___closed__1; uint8_t lean_usize_dec_lt(size_t, size_t); @@ -23035,18 +23035,25 @@ x_42 = lean_unbox(x_41); lean_dec(x_41); if (x_42 == 0) { -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_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; x_43 = lean_ctor_get(x_40, 1); lean_inc(x_43); lean_dec(x_40); lean_inc(x_3); +lean_inc(x_20); lean_ctor_set(x_6, 1, x_3); x_44 = l_Lean_Elab_Tactic_setGoals(x_6, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_43); x_45 = lean_ctor_get(x_44, 1); lean_inc(x_45); lean_dec(x_44); -x_46 = lean_unsigned_to_nat(1u); -x_47 = l_Lean_Syntax_getArg(x_1, x_46); +x_46 = l_Lean_Elab_Tactic_saveState___rarg(x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_45); +x_47 = lean_ctor_get(x_46, 0); +lean_inc(x_47); +x_48 = lean_ctor_get(x_46, 1); +lean_inc(x_48); +lean_dec(x_46); +x_49 = lean_unsigned_to_nat(1u); +x_50 = l_Lean_Syntax_getArg(x_1, x_49); lean_inc(x_16); lean_inc(x_15); lean_inc(x_14); @@ -23055,43 +23062,47 @@ lean_inc(x_12); lean_inc(x_11); lean_inc(x_10); lean_inc(x_9); -x_48 = l_Lean_Elab_Tactic_evalTactic(x_47, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_45); -if (lean_obj_tag(x_48) == 0) +x_51 = l_Lean_Elab_Tactic_evalTactic(x_50, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_48); +if (lean_obj_tag(x_51) == 0) { -lean_object* x_49; uint8_t x_50; -x_49 = lean_ctor_get(x_48, 1); -lean_inc(x_49); -lean_dec(x_48); -x_50 = lean_unbox(x_27); +lean_object* x_52; uint8_t x_53; +lean_dec(x_47); +lean_dec(x_20); +x_52 = lean_ctor_get(x_51, 1); +lean_inc(x_52); +lean_dec(x_51); +x_53 = lean_unbox(x_27); lean_dec(x_27); -x_30 = x_50; -x_31 = x_49; +x_30 = x_53; +x_31 = x_52; goto block_39; } else { -uint8_t x_51; +uint8_t x_54; lean_dec(x_27); -x_51 = !lean_is_exclusive(x_48); -if (x_51 == 0) -{ -lean_object* x_52; lean_object* x_53; uint8_t x_54; -x_52 = lean_ctor_get(x_48, 0); -x_53 = lean_ctor_get(x_48, 1); -x_54 = l_Lean_Exception_isInterrupt(x_52); +x_54 = !lean_is_exclusive(x_51); if (x_54 == 0) { -uint8_t x_55; -x_55 = l_Lean_Exception_isRuntime(x_52); -if (x_55 == 0) +lean_object* x_55; lean_object* x_56; uint8_t x_57; +x_55 = lean_ctor_get(x_51, 0); +x_56 = lean_ctor_get(x_51, 1); +x_57 = l_Lean_Exception_isInterrupt(x_55); +if (x_57 == 0) { -uint8_t x_56; -x_56 = lean_ctor_get_uint8(x_9, sizeof(void*)*1); -if (x_56 == 0) +uint8_t x_58; +x_58 = l_Lean_Exception_isRuntime(x_55); +if (x_58 == 0) { +uint8_t x_59; +x_59 = lean_ctor_get_uint8(x_9, sizeof(void*)*1); +if (x_59 == 0) +{ +lean_dec(x_47); lean_dec(x_29); lean_dec(x_28); lean_dec(x_21); +lean_dec(x_20); lean_dec(x_16); lean_dec(x_15); lean_dec(x_14); @@ -23101,137 +23112,40 @@ lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_3); -return x_48; +return x_51; } else { -lean_object* x_57; -lean_free_object(x_48); +lean_object* x_60; +lean_free_object(x_51); lean_inc(x_15); -x_57 = l_Lean_Elab_logException___at_Lean_Elab_Tactic_closeUsingOrAdmit___spec__1(x_52, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_53); -if (lean_obj_tag(x_57) == 0) +x_60 = l_Lean_Elab_logException___at_Lean_Elab_Tactic_closeUsingOrAdmit___spec__1(x_55, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_56); +if (lean_obj_tag(x_60) == 0) { -lean_object* x_58; uint8_t x_59; -x_58 = lean_ctor_get(x_57, 1); -lean_inc(x_58); -lean_dec(x_57); -x_59 = 1; -x_30 = x_59; -x_31 = x_58; -goto block_39; -} -else -{ -uint8_t x_60; -lean_dec(x_29); -lean_dec(x_28); -lean_dec(x_21); -lean_dec(x_16); -lean_dec(x_15); -lean_dec(x_14); -lean_dec(x_13); -lean_dec(x_12); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_3); -x_60 = !lean_is_exclusive(x_57); -if (x_60 == 0) -{ -return x_57; -} -else -{ -lean_object* x_61; lean_object* x_62; lean_object* x_63; -x_61 = lean_ctor_get(x_57, 0); -x_62 = lean_ctor_get(x_57, 1); -lean_inc(x_62); +lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; uint8_t x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; +x_61 = lean_ctor_get(x_60, 1); lean_inc(x_61); -lean_dec(x_57); -x_63 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_63, 0, x_61); -lean_ctor_set(x_63, 1, x_62); -return x_63; -} -} -} -} -else -{ -lean_dec(x_29); -lean_dec(x_28); -lean_dec(x_21); -lean_dec(x_16); -lean_dec(x_15); -lean_dec(x_14); -lean_dec(x_13); -lean_dec(x_12); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_3); -return x_48; -} -} -else -{ -lean_dec(x_29); -lean_dec(x_28); -lean_dec(x_21); -lean_dec(x_16); -lean_dec(x_15); -lean_dec(x_14); -lean_dec(x_13); -lean_dec(x_12); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_3); -return x_48; -} -} -else -{ -lean_object* x_64; lean_object* x_65; uint8_t x_66; -x_64 = lean_ctor_get(x_48, 0); -x_65 = lean_ctor_get(x_48, 1); -lean_inc(x_65); +lean_dec(x_60); +x_62 = l_Lean_Core_getMessageLog___rarg(x_16, x_61); +x_63 = lean_ctor_get(x_62, 0); +lean_inc(x_63); +x_64 = lean_ctor_get(x_62, 1); lean_inc(x_64); -lean_dec(x_48); -x_66 = l_Lean_Exception_isInterrupt(x_64); -if (x_66 == 0) -{ -uint8_t x_67; -x_67 = l_Lean_Exception_isRuntime(x_64); -if (x_67 == 0) -{ -uint8_t x_68; -x_68 = lean_ctor_get_uint8(x_9, sizeof(void*)*1); -if (x_68 == 0) -{ -lean_object* x_69; -lean_dec(x_29); -lean_dec(x_28); -lean_dec(x_21); -lean_dec(x_16); -lean_dec(x_15); -lean_dec(x_14); -lean_dec(x_13); -lean_dec(x_12); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_3); -x_69 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_69, 0, x_64); -lean_ctor_set(x_69, 1, x_65); -return x_69; -} -else -{ -lean_object* x_70; +lean_dec(x_62); +x_65 = 0; +x_66 = l_Lean_Elab_Tactic_SavedState_restore(x_47, x_65, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_64); +x_67 = lean_ctor_get(x_66, 1); +lean_inc(x_67); +lean_dec(x_66); +x_68 = l_Lean_Core_setMessageLog(x_63, x_15, x_16, x_67); +x_69 = lean_ctor_get(x_68, 1); +lean_inc(x_69); +lean_dec(x_68); +lean_inc(x_16); lean_inc(x_15); -x_70 = l_Lean_Elab_logException___at_Lean_Elab_Tactic_closeUsingOrAdmit___spec__1(x_64, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_65); +lean_inc(x_14); +lean_inc(x_13); +x_70 = l_Lean_Elab_admitGoal(x_20, x_13, x_14, x_15, x_16, x_69); if (lean_obj_tag(x_70) == 0) { lean_object* x_71; uint8_t x_72; @@ -23245,7 +23159,7 @@ goto block_39; } else { -lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; +uint8_t x_73; lean_dec(x_29); lean_dec(x_28); lean_dec(x_21); @@ -23258,32 +23172,186 @@ lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_3); -x_73 = lean_ctor_get(x_70, 0); -lean_inc(x_73); -x_74 = lean_ctor_get(x_70, 1); +x_73 = !lean_is_exclusive(x_70); +if (x_73 == 0) +{ +return x_70; +} +else +{ +lean_object* x_74; lean_object* x_75; lean_object* x_76; +x_74 = lean_ctor_get(x_70, 0); +x_75 = lean_ctor_get(x_70, 1); +lean_inc(x_75); lean_inc(x_74); -if (lean_is_exclusive(x_70)) { - lean_ctor_release(x_70, 0); - lean_ctor_release(x_70, 1); - x_75 = x_70; -} else { - lean_dec_ref(x_70); - x_75 = lean_box(0); -} -if (lean_is_scalar(x_75)) { - x_76 = lean_alloc_ctor(1, 2, 0); -} else { - x_76 = x_75; -} -lean_ctor_set(x_76, 0, x_73); -lean_ctor_set(x_76, 1, x_74); +lean_dec(x_70); +x_76 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_76, 0, x_74); +lean_ctor_set(x_76, 1, x_75); return x_76; } } } else { -lean_object* x_77; +uint8_t x_77; +lean_dec(x_47); +lean_dec(x_29); +lean_dec(x_28); +lean_dec(x_21); +lean_dec(x_20); +lean_dec(x_16); +lean_dec(x_15); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_3); +x_77 = !lean_is_exclusive(x_60); +if (x_77 == 0) +{ +return x_60; +} +else +{ +lean_object* x_78; lean_object* x_79; lean_object* x_80; +x_78 = lean_ctor_get(x_60, 0); +x_79 = lean_ctor_get(x_60, 1); +lean_inc(x_79); +lean_inc(x_78); +lean_dec(x_60); +x_80 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_80, 0, x_78); +lean_ctor_set(x_80, 1, x_79); +return x_80; +} +} +} +} +else +{ +lean_dec(x_47); +lean_dec(x_29); +lean_dec(x_28); +lean_dec(x_21); +lean_dec(x_20); +lean_dec(x_16); +lean_dec(x_15); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_3); +return x_51; +} +} +else +{ +lean_dec(x_47); +lean_dec(x_29); +lean_dec(x_28); +lean_dec(x_21); +lean_dec(x_20); +lean_dec(x_16); +lean_dec(x_15); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_3); +return x_51; +} +} +else +{ +lean_object* x_81; lean_object* x_82; uint8_t x_83; +x_81 = lean_ctor_get(x_51, 0); +x_82 = lean_ctor_get(x_51, 1); +lean_inc(x_82); +lean_inc(x_81); +lean_dec(x_51); +x_83 = l_Lean_Exception_isInterrupt(x_81); +if (x_83 == 0) +{ +uint8_t x_84; +x_84 = l_Lean_Exception_isRuntime(x_81); +if (x_84 == 0) +{ +uint8_t x_85; +x_85 = lean_ctor_get_uint8(x_9, sizeof(void*)*1); +if (x_85 == 0) +{ +lean_object* x_86; +lean_dec(x_47); +lean_dec(x_29); +lean_dec(x_28); +lean_dec(x_21); +lean_dec(x_20); +lean_dec(x_16); +lean_dec(x_15); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_3); +x_86 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_86, 0, x_81); +lean_ctor_set(x_86, 1, x_82); +return x_86; +} +else +{ +lean_object* x_87; +lean_inc(x_15); +x_87 = l_Lean_Elab_logException___at_Lean_Elab_Tactic_closeUsingOrAdmit___spec__1(x_81, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_82); +if (lean_obj_tag(x_87) == 0) +{ +lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; uint8_t x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; +x_88 = lean_ctor_get(x_87, 1); +lean_inc(x_88); +lean_dec(x_87); +x_89 = l_Lean_Core_getMessageLog___rarg(x_16, x_88); +x_90 = lean_ctor_get(x_89, 0); +lean_inc(x_90); +x_91 = lean_ctor_get(x_89, 1); +lean_inc(x_91); +lean_dec(x_89); +x_92 = 0; +x_93 = l_Lean_Elab_Tactic_SavedState_restore(x_47, x_92, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_91); +x_94 = lean_ctor_get(x_93, 1); +lean_inc(x_94); +lean_dec(x_93); +x_95 = l_Lean_Core_setMessageLog(x_90, x_15, x_16, x_94); +x_96 = lean_ctor_get(x_95, 1); +lean_inc(x_96); +lean_dec(x_95); +lean_inc(x_16); +lean_inc(x_15); +lean_inc(x_14); +lean_inc(x_13); +x_97 = l_Lean_Elab_admitGoal(x_20, x_13, x_14, x_15, x_16, x_96); +if (lean_obj_tag(x_97) == 0) +{ +lean_object* x_98; uint8_t x_99; +x_98 = lean_ctor_get(x_97, 1); +lean_inc(x_98); +lean_dec(x_97); +x_99 = 1; +x_30 = x_99; +x_31 = x_98; +goto block_39; +} +else +{ +lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_dec(x_29); lean_dec(x_28); lean_dec(x_21); @@ -23296,18 +23364,36 @@ lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_3); -x_77 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_77, 0, x_64); -lean_ctor_set(x_77, 1, x_65); -return x_77; +x_100 = lean_ctor_get(x_97, 0); +lean_inc(x_100); +x_101 = lean_ctor_get(x_97, 1); +lean_inc(x_101); +if (lean_is_exclusive(x_97)) { + lean_ctor_release(x_97, 0); + lean_ctor_release(x_97, 1); + x_102 = x_97; +} else { + lean_dec_ref(x_97); + x_102 = lean_box(0); +} +if (lean_is_scalar(x_102)) { + x_103 = lean_alloc_ctor(1, 2, 0); +} else { + x_103 = x_102; +} +lean_ctor_set(x_103, 0, x_100); +lean_ctor_set(x_103, 1, x_101); +return x_103; } } else { -lean_object* x_78; +lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; +lean_dec(x_47); lean_dec(x_29); lean_dec(x_28); lean_dec(x_21); +lean_dec(x_20); lean_dec(x_16); lean_dec(x_15); lean_dec(x_14); @@ -23317,48 +23403,111 @@ lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_3); -x_78 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_78, 0, x_64); -lean_ctor_set(x_78, 1, x_65); -return x_78; +x_104 = lean_ctor_get(x_87, 0); +lean_inc(x_104); +x_105 = lean_ctor_get(x_87, 1); +lean_inc(x_105); +if (lean_is_exclusive(x_87)) { + lean_ctor_release(x_87, 0); + lean_ctor_release(x_87, 1); + x_106 = x_87; +} else { + lean_dec_ref(x_87); + x_106 = lean_box(0); +} +if (lean_is_scalar(x_106)) { + x_107 = lean_alloc_ctor(1, 2, 0); +} else { + x_107 = x_106; +} +lean_ctor_set(x_107, 0, x_104); +lean_ctor_set(x_107, 1, x_105); +return x_107; +} +} +} +else +{ +lean_object* x_108; +lean_dec(x_47); +lean_dec(x_29); +lean_dec(x_28); +lean_dec(x_21); +lean_dec(x_20); +lean_dec(x_16); +lean_dec(x_15); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_3); +x_108 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_108, 0, x_81); +lean_ctor_set(x_108, 1, x_82); +return x_108; +} +} +else +{ +lean_object* x_109; +lean_dec(x_47); +lean_dec(x_29); +lean_dec(x_28); +lean_dec(x_21); +lean_dec(x_20); +lean_dec(x_16); +lean_dec(x_15); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_3); +x_109 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_109, 0, x_81); +lean_ctor_set(x_109, 1, x_82); +return x_109; } } } } else { -uint8_t x_79; +uint8_t x_110; lean_dec(x_29); lean_free_object(x_6); lean_dec(x_20); -x_79 = !lean_is_exclusive(x_40); -if (x_79 == 0) +x_110 = !lean_is_exclusive(x_40); +if (x_110 == 0) { -lean_object* x_80; lean_object* x_81; lean_object* x_82; -x_80 = lean_ctor_get(x_40, 1); -x_81 = lean_ctor_get(x_40, 0); -lean_dec(x_81); +lean_object* x_111; lean_object* x_112; lean_object* x_113; +x_111 = lean_ctor_get(x_40, 1); +x_112 = lean_ctor_get(x_40, 0); +lean_dec(x_112); lean_ctor_set(x_40, 1, x_28); lean_ctor_set(x_40, 0, x_27); -x_82 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_82, 0, x_40); -x_22 = x_82; -x_23 = x_80; +x_113 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_113, 0, x_40); +x_22 = x_113; +x_23 = x_111; goto block_26; } else { -lean_object* x_83; lean_object* x_84; lean_object* x_85; -x_83 = lean_ctor_get(x_40, 1); -lean_inc(x_83); +lean_object* x_114; lean_object* x_115; lean_object* x_116; +x_114 = lean_ctor_get(x_40, 1); +lean_inc(x_114); lean_dec(x_40); -x_84 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_84, 0, x_27); -lean_ctor_set(x_84, 1, x_28); -x_85 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_85, 0, x_84); -x_22 = x_85; -x_23 = x_83; +x_115 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_115, 0, x_27); +lean_ctor_set(x_115, 1, x_28); +x_116 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_116, 0, x_115); +x_22 = x_116; +x_23 = x_114; goto block_26; } } @@ -23401,45 +23550,52 @@ goto block_26; } else { -lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_93; lean_object* x_94; lean_object* x_95; uint8_t x_96; lean_object* x_97; lean_object* x_106; lean_object* x_107; uint8_t x_108; -x_86 = lean_ctor_get(x_6, 0); -x_87 = lean_ctor_get(x_6, 1); -lean_inc(x_87); -lean_inc(x_86); +lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_124; lean_object* x_125; lean_object* x_126; uint8_t x_127; lean_object* x_128; lean_object* x_137; lean_object* x_138; uint8_t x_139; +x_117 = lean_ctor_get(x_6, 0); +x_118 = lean_ctor_get(x_6, 1); +lean_inc(x_118); +lean_inc(x_117); lean_dec(x_6); -x_93 = lean_ctor_get(x_7, 0); -lean_inc(x_93); -x_94 = lean_ctor_get(x_7, 1); -lean_inc(x_94); +x_124 = lean_ctor_get(x_7, 0); +lean_inc(x_124); +x_125 = lean_ctor_get(x_7, 1); +lean_inc(x_125); if (lean_is_exclusive(x_7)) { lean_ctor_release(x_7, 0); lean_ctor_release(x_7, 1); - x_95 = x_7; + x_126 = x_7; } else { lean_dec_ref(x_7); - x_95 = lean_box(0); + x_126 = lean_box(0); } -x_106 = l_Lean_MVarId_isAssigned___at_Lean_Elab_Tactic_pruneSolvedGoals___spec__1(x_86, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_17); -x_107 = lean_ctor_get(x_106, 0); -lean_inc(x_107); -x_108 = lean_unbox(x_107); -lean_dec(x_107); -if (x_108 == 0) +x_137 = l_Lean_MVarId_isAssigned___at_Lean_Elab_Tactic_pruneSolvedGoals___spec__1(x_117, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_17); +x_138 = lean_ctor_get(x_137, 0); +lean_inc(x_138); +x_139 = lean_unbox(x_138); +lean_dec(x_138); +if (x_139 == 0) { -lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; -x_109 = lean_ctor_get(x_106, 1); -lean_inc(x_109); -lean_dec(x_106); +lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; +x_140 = lean_ctor_get(x_137, 1); +lean_inc(x_140); +lean_dec(x_137); lean_inc(x_3); -x_110 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_110, 0, x_86); -lean_ctor_set(x_110, 1, x_3); -x_111 = l_Lean_Elab_Tactic_setGoals(x_110, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_109); -x_112 = lean_ctor_get(x_111, 1); -lean_inc(x_112); -lean_dec(x_111); -x_113 = lean_unsigned_to_nat(1u); -x_114 = l_Lean_Syntax_getArg(x_1, x_113); +lean_inc(x_117); +x_141 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_141, 0, x_117); +lean_ctor_set(x_141, 1, x_3); +x_142 = l_Lean_Elab_Tactic_setGoals(x_141, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_140); +x_143 = lean_ctor_get(x_142, 1); +lean_inc(x_143); +lean_dec(x_142); +x_144 = l_Lean_Elab_Tactic_saveState___rarg(x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_143); +x_145 = lean_ctor_get(x_144, 0); +lean_inc(x_145); +x_146 = lean_ctor_get(x_144, 1); +lean_inc(x_146); +lean_dec(x_144); +x_147 = lean_unsigned_to_nat(1u); +x_148 = l_Lean_Syntax_getArg(x_1, x_147); lean_inc(x_16); lean_inc(x_15); lean_inc(x_14); @@ -23448,91 +23604,54 @@ lean_inc(x_12); lean_inc(x_11); lean_inc(x_10); lean_inc(x_9); -x_115 = l_Lean_Elab_Tactic_evalTactic(x_114, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_112); -if (lean_obj_tag(x_115) == 0) +x_149 = l_Lean_Elab_Tactic_evalTactic(x_148, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_146); +if (lean_obj_tag(x_149) == 0) { -lean_object* x_116; uint8_t x_117; -x_116 = lean_ctor_get(x_115, 1); -lean_inc(x_116); -lean_dec(x_115); -x_117 = lean_unbox(x_93); -lean_dec(x_93); -x_96 = x_117; -x_97 = x_116; -goto block_105; +lean_object* x_150; uint8_t x_151; +lean_dec(x_145); +lean_dec(x_117); +x_150 = lean_ctor_get(x_149, 1); +lean_inc(x_150); +lean_dec(x_149); +x_151 = lean_unbox(x_124); +lean_dec(x_124); +x_127 = x_151; +x_128 = x_150; +goto block_136; } else { -lean_object* x_118; lean_object* x_119; lean_object* x_120; uint8_t x_121; -lean_dec(x_93); -x_118 = lean_ctor_get(x_115, 0); -lean_inc(x_118); -x_119 = lean_ctor_get(x_115, 1); -lean_inc(x_119); -if (lean_is_exclusive(x_115)) { - lean_ctor_release(x_115, 0); - lean_ctor_release(x_115, 1); - x_120 = x_115; +lean_object* x_152; lean_object* x_153; lean_object* x_154; uint8_t x_155; +lean_dec(x_124); +x_152 = lean_ctor_get(x_149, 0); +lean_inc(x_152); +x_153 = lean_ctor_get(x_149, 1); +lean_inc(x_153); +if (lean_is_exclusive(x_149)) { + lean_ctor_release(x_149, 0); + lean_ctor_release(x_149, 1); + x_154 = x_149; } else { - lean_dec_ref(x_115); - x_120 = lean_box(0); + lean_dec_ref(x_149); + x_154 = lean_box(0); } -x_121 = l_Lean_Exception_isInterrupt(x_118); -if (x_121 == 0) +x_155 = l_Lean_Exception_isInterrupt(x_152); +if (x_155 == 0) { -uint8_t x_122; -x_122 = l_Lean_Exception_isRuntime(x_118); -if (x_122 == 0) +uint8_t x_156; +x_156 = l_Lean_Exception_isRuntime(x_152); +if (x_156 == 0) { -uint8_t x_123; -x_123 = lean_ctor_get_uint8(x_9, sizeof(void*)*1); -if (x_123 == 0) +uint8_t x_157; +x_157 = lean_ctor_get_uint8(x_9, sizeof(void*)*1); +if (x_157 == 0) { -lean_object* x_124; -lean_dec(x_95); -lean_dec(x_94); -lean_dec(x_87); -lean_dec(x_16); -lean_dec(x_15); -lean_dec(x_14); -lean_dec(x_13); -lean_dec(x_12); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_3); -if (lean_is_scalar(x_120)) { - x_124 = lean_alloc_ctor(1, 2, 0); -} else { - x_124 = x_120; -} -lean_ctor_set(x_124, 0, x_118); -lean_ctor_set(x_124, 1, x_119); -return x_124; -} -else -{ -lean_object* x_125; -lean_dec(x_120); -lean_inc(x_15); -x_125 = l_Lean_Elab_logException___at_Lean_Elab_Tactic_closeUsingOrAdmit___spec__1(x_118, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_119); -if (lean_obj_tag(x_125) == 0) -{ -lean_object* x_126; uint8_t x_127; -x_126 = lean_ctor_get(x_125, 1); -lean_inc(x_126); +lean_object* x_158; +lean_dec(x_145); +lean_dec(x_126); lean_dec(x_125); -x_127 = 1; -x_96 = x_127; -x_97 = x_126; -goto block_105; -} -else -{ -lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; -lean_dec(x_95); -lean_dec(x_94); -lean_dec(x_87); +lean_dec(x_118); +lean_dec(x_117); lean_dec(x_16); lean_dec(x_15); lean_dec(x_14); @@ -23542,241 +23661,259 @@ lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_3); -x_128 = lean_ctor_get(x_125, 0); -lean_inc(x_128); -x_129 = lean_ctor_get(x_125, 1); -lean_inc(x_129); -if (lean_is_exclusive(x_125)) { - lean_ctor_release(x_125, 0); - lean_ctor_release(x_125, 1); - x_130 = x_125; +if (lean_is_scalar(x_154)) { + x_158 = lean_alloc_ctor(1, 2, 0); } else { - lean_dec_ref(x_125); - x_130 = lean_box(0); -} -if (lean_is_scalar(x_130)) { - x_131 = lean_alloc_ctor(1, 2, 0); -} else { - x_131 = x_130; -} -lean_ctor_set(x_131, 0, x_128); -lean_ctor_set(x_131, 1, x_129); -return x_131; -} + x_158 = x_154; } +lean_ctor_set(x_158, 0, x_152); +lean_ctor_set(x_158, 1, x_153); +return x_158; } else { -lean_object* x_132; -lean_dec(x_95); -lean_dec(x_94); -lean_dec(x_87); -lean_dec(x_16); -lean_dec(x_15); -lean_dec(x_14); -lean_dec(x_13); -lean_dec(x_12); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_3); -if (lean_is_scalar(x_120)) { - x_132 = lean_alloc_ctor(1, 2, 0); -} else { - x_132 = x_120; -} -lean_ctor_set(x_132, 0, x_118); -lean_ctor_set(x_132, 1, x_119); -return x_132; -} -} -else +lean_object* x_159; +lean_dec(x_154); +lean_inc(x_15); +x_159 = l_Lean_Elab_logException___at_Lean_Elab_Tactic_closeUsingOrAdmit___spec__1(x_152, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_153); +if (lean_obj_tag(x_159) == 0) { -lean_object* x_133; -lean_dec(x_95); -lean_dec(x_94); -lean_dec(x_87); -lean_dec(x_16); -lean_dec(x_15); -lean_dec(x_14); -lean_dec(x_13); -lean_dec(x_12); -lean_dec(x_11); -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_3); -if (lean_is_scalar(x_120)) { - x_133 = lean_alloc_ctor(1, 2, 0); -} else { - x_133 = x_120; -} -lean_ctor_set(x_133, 0, x_118); -lean_ctor_set(x_133, 1, x_119); -return x_133; -} -} -} -else -{ -lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; -lean_dec(x_95); -lean_dec(x_86); -x_134 = lean_ctor_get(x_106, 1); -lean_inc(x_134); -if (lean_is_exclusive(x_106)) { - lean_ctor_release(x_106, 0); - lean_ctor_release(x_106, 1); - x_135 = x_106; -} else { - lean_dec_ref(x_106); - x_135 = lean_box(0); -} -if (lean_is_scalar(x_135)) { - x_136 = lean_alloc_ctor(0, 2, 0); -} else { - x_136 = x_135; -} -lean_ctor_set(x_136, 0, x_93); -lean_ctor_set(x_136, 1, x_94); -x_137 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_137, 0, x_136); -x_88 = x_137; -x_89 = x_134; -goto block_92; -} -block_92: -{ -lean_object* x_90; -x_90 = lean_ctor_get(x_88, 0); -lean_inc(x_90); -lean_dec(x_88); -x_6 = x_87; -x_7 = x_90; -x_8 = lean_box(0); -x_17 = x_89; -goto _start; -} -block_105: -{ -lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; -x_98 = l_Lean_Elab_Tactic_getUnsolvedGoals(x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_97); -x_99 = lean_ctor_get(x_98, 0); -lean_inc(x_99); -x_100 = lean_ctor_get(x_98, 1); -lean_inc(x_100); -lean_dec(x_98); -x_101 = l_List_foldl___at_Array_appendList___spec__1___rarg(x_94, x_99); -x_102 = lean_box(x_96); -if (lean_is_scalar(x_95)) { - x_103 = lean_alloc_ctor(0, 2, 0); -} else { - x_103 = x_95; -} -lean_ctor_set(x_103, 0, x_102); -lean_ctor_set(x_103, 1, x_101); -x_104 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_104, 0, x_103); -x_88 = x_104; -x_89 = x_100; -goto block_92; -} -} -} -} -} -LEAN_EXPORT lean_object* l_List_forM___at_Lean_Elab_Tactic_evalAllGoals___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, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) { -_start: -{ -if (lean_obj_tag(x_1) == 0) -{ -lean_object* x_11; lean_object* x_12; -lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -x_11 = lean_box(0); -x_12 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_12, 0, x_11); -lean_ctor_set(x_12, 1, x_10); -return x_12; -} -else -{ -lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; -x_13 = lean_ctor_get(x_1, 0); -lean_inc(x_13); -x_14 = lean_ctor_get(x_1, 1); -lean_inc(x_14); -lean_dec(x_1); -x_15 = l_Lean_MVarId_isAssigned___at_Lean_Elab_Tactic_pruneSolvedGoals___spec__1(x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10); -x_16 = lean_ctor_get(x_15, 0); +lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; uint8_t x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; +x_160 = lean_ctor_get(x_159, 1); +lean_inc(x_160); +lean_dec(x_159); +x_161 = l_Lean_Core_getMessageLog___rarg(x_16, x_160); +x_162 = lean_ctor_get(x_161, 0); +lean_inc(x_162); +x_163 = lean_ctor_get(x_161, 1); +lean_inc(x_163); +lean_dec(x_161); +x_164 = 0; +x_165 = l_Lean_Elab_Tactic_SavedState_restore(x_145, x_164, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_163); +x_166 = lean_ctor_get(x_165, 1); +lean_inc(x_166); +lean_dec(x_165); +x_167 = l_Lean_Core_setMessageLog(x_162, x_15, x_16, x_166); +x_168 = lean_ctor_get(x_167, 1); +lean_inc(x_168); +lean_dec(x_167); lean_inc(x_16); -x_17 = lean_unbox(x_16); +lean_inc(x_15); +lean_inc(x_14); +lean_inc(x_13); +x_169 = l_Lean_Elab_admitGoal(x_117, x_13, x_14, x_15, x_16, x_168); +if (lean_obj_tag(x_169) == 0) +{ +lean_object* x_170; uint8_t x_171; +x_170 = lean_ctor_get(x_169, 1); +lean_inc(x_170); +lean_dec(x_169); +x_171 = 1; +x_127 = x_171; +x_128 = x_170; +goto block_136; +} +else +{ +lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; +lean_dec(x_126); +lean_dec(x_125); +lean_dec(x_118); lean_dec(x_16); -if (x_17 == 0) -{ -lean_object* x_18; lean_object* x_19; -x_18 = lean_ctor_get(x_15, 1); -lean_inc(x_18); lean_dec(x_15); -lean_inc(x_9); -lean_inc(x_8); -lean_inc(x_7); -lean_inc(x_6); -x_19 = l_Lean_Elab_admitGoal(x_13, x_6, x_7, x_8, x_9, x_18); -if (lean_obj_tag(x_19) == 0) -{ -lean_object* x_20; -x_20 = lean_ctor_get(x_19, 1); -lean_inc(x_20); -lean_dec(x_19); -x_1 = x_14; -x_10 = x_20; -goto _start; -} -else -{ -uint8_t x_22; lean_dec(x_14); -lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -x_22 = !lean_is_exclusive(x_19); -if (x_22 == 0) -{ -return x_19; -} -else -{ -lean_object* x_23; lean_object* x_24; lean_object* x_25; -x_23 = lean_ctor_get(x_19, 0); -x_24 = lean_ctor_get(x_19, 1); -lean_inc(x_24); -lean_inc(x_23); -lean_dec(x_19); -x_25 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_25, 0, x_23); -lean_ctor_set(x_25, 1, x_24); -return x_25; -} -} -} -else -{ -lean_object* x_26; lean_dec(x_13); -x_26 = lean_ctor_get(x_15, 1); -lean_inc(x_26); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_3); +x_172 = lean_ctor_get(x_169, 0); +lean_inc(x_172); +x_173 = lean_ctor_get(x_169, 1); +lean_inc(x_173); +if (lean_is_exclusive(x_169)) { + lean_ctor_release(x_169, 0); + lean_ctor_release(x_169, 1); + x_174 = x_169; +} else { + lean_dec_ref(x_169); + x_174 = lean_box(0); +} +if (lean_is_scalar(x_174)) { + x_175 = lean_alloc_ctor(1, 2, 0); +} else { + x_175 = x_174; +} +lean_ctor_set(x_175, 0, x_172); +lean_ctor_set(x_175, 1, x_173); +return x_175; +} +} +else +{ +lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; +lean_dec(x_145); +lean_dec(x_126); +lean_dec(x_125); +lean_dec(x_118); +lean_dec(x_117); +lean_dec(x_16); lean_dec(x_15); -x_1 = x_14; -x_10 = x_26; +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_3); +x_176 = lean_ctor_get(x_159, 0); +lean_inc(x_176); +x_177 = lean_ctor_get(x_159, 1); +lean_inc(x_177); +if (lean_is_exclusive(x_159)) { + lean_ctor_release(x_159, 0); + lean_ctor_release(x_159, 1); + x_178 = x_159; +} else { + lean_dec_ref(x_159); + x_178 = lean_box(0); +} +if (lean_is_scalar(x_178)) { + x_179 = lean_alloc_ctor(1, 2, 0); +} else { + x_179 = x_178; +} +lean_ctor_set(x_179, 0, x_176); +lean_ctor_set(x_179, 1, x_177); +return x_179; +} +} +} +else +{ +lean_object* x_180; +lean_dec(x_145); +lean_dec(x_126); +lean_dec(x_125); +lean_dec(x_118); +lean_dec(x_117); +lean_dec(x_16); +lean_dec(x_15); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_3); +if (lean_is_scalar(x_154)) { + x_180 = lean_alloc_ctor(1, 2, 0); +} else { + x_180 = x_154; +} +lean_ctor_set(x_180, 0, x_152); +lean_ctor_set(x_180, 1, x_153); +return x_180; +} +} +else +{ +lean_object* x_181; +lean_dec(x_145); +lean_dec(x_126); +lean_dec(x_125); +lean_dec(x_118); +lean_dec(x_117); +lean_dec(x_16); +lean_dec(x_15); +lean_dec(x_14); +lean_dec(x_13); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_3); +if (lean_is_scalar(x_154)) { + x_181 = lean_alloc_ctor(1, 2, 0); +} else { + x_181 = x_154; +} +lean_ctor_set(x_181, 0, x_152); +lean_ctor_set(x_181, 1, x_153); +return x_181; +} +} +} +else +{ +lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; +lean_dec(x_126); +lean_dec(x_117); +x_182 = lean_ctor_get(x_137, 1); +lean_inc(x_182); +if (lean_is_exclusive(x_137)) { + lean_ctor_release(x_137, 0); + lean_ctor_release(x_137, 1); + x_183 = x_137; +} else { + lean_dec_ref(x_137); + x_183 = lean_box(0); +} +if (lean_is_scalar(x_183)) { + x_184 = lean_alloc_ctor(0, 2, 0); +} else { + x_184 = x_183; +} +lean_ctor_set(x_184, 0, x_124); +lean_ctor_set(x_184, 1, x_125); +x_185 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_185, 0, x_184); +x_119 = x_185; +x_120 = x_182; +goto block_123; +} +block_123: +{ +lean_object* x_121; +x_121 = lean_ctor_get(x_119, 0); +lean_inc(x_121); +lean_dec(x_119); +x_6 = x_118; +x_7 = x_121; +x_8 = lean_box(0); +x_17 = x_120; goto _start; } +block_136: +{ +lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; +x_129 = l_Lean_Elab_Tactic_getUnsolvedGoals(x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_128); +x_130 = lean_ctor_get(x_129, 0); +lean_inc(x_130); +x_131 = lean_ctor_get(x_129, 1); +lean_inc(x_131); +lean_dec(x_129); +x_132 = l_List_foldl___at_Array_appendList___spec__1___rarg(x_125, x_130); +x_133 = lean_box(x_127); +if (lean_is_scalar(x_126)) { + x_134 = lean_alloc_ctor(0, 2, 0); +} else { + x_134 = x_126; +} +lean_ctor_set(x_134, 0, x_133); +lean_ctor_set(x_134, 1, x_132); +x_135 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_135, 0, x_134); +x_119 = x_135; +x_120 = x_131; +goto block_123; } } } -static lean_object* _init_l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__1() { +} +} +static lean_object* _init_l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__1() { _start: { lean_object* x_1; @@ -23784,34 +23921,34 @@ x_1 = l_Lean_Elab_abortTacticExceptionId; return x_1; } } -static lean_object* _init_l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__2() { +static lean_object* _init_l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__1; +x_2 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__1; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__2; +x_2 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__2; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___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, lean_object* x_8) { +LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___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, lean_object* x_7, lean_object* x_8) { _start: { lean_object* x_9; -x_9 = lean_alloc_closure((void*)(l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg), 1, 0); +x_9 = lean_alloc_closure((void*)(l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg), 1, 0); return x_9; } } @@ -23840,7 +23977,7 @@ return x_4; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAllGoals(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) { _start: { -lean_object* x_11; 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_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; x_11 = l_Lean_Elab_Tactic_getGoals___rarg(x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10); x_12 = lean_ctor_get(x_11, 0); lean_inc(x_12); @@ -23848,17 +23985,8 @@ x_13 = lean_ctor_get(x_11, 1); lean_inc(x_13); lean_dec(x_11); x_14 = lean_box(0); -x_15 = lean_st_ref_get(x_7, x_13); -x_16 = lean_ctor_get(x_15, 0); -lean_inc(x_16); -x_17 = lean_ctor_get(x_15, 1); -lean_inc(x_17); -lean_dec(x_15); -x_18 = lean_ctor_get(x_16, 0); -lean_inc(x_18); -lean_dec(x_16); -x_19 = lean_box(0); -x_20 = l_Lean_Elab_Tactic_evalAllGoals___closed__1; +x_15 = lean_box(0); +x_16 = l_Lean_Elab_Tactic_evalAllGoals___closed__1; lean_inc(x_9); lean_inc(x_8); lean_inc(x_7); @@ -23868,204 +23996,77 @@ lean_inc(x_4); lean_inc(x_3); lean_inc(x_2); lean_inc(x_12); -x_21 = l_List_forIn_x27_loop___at_Lean_Elab_Tactic_evalAllGoals___spec__1(x_1, x_12, x_14, x_19, x_12, x_12, x_20, lean_box(0), x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_17); -if (lean_obj_tag(x_21) == 0) +x_17 = l_List_forIn_x27_loop___at_Lean_Elab_Tactic_evalAllGoals___spec__1(x_1, x_12, x_14, x_15, x_12, x_12, x_16, lean_box(0), x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13); +lean_dec(x_12); +if (lean_obj_tag(x_17) == 0) { -lean_object* x_22; lean_object* x_23; uint8_t x_24; -x_22 = lean_ctor_get(x_21, 0); +lean_object* x_18; lean_object* x_19; uint8_t x_20; +x_18 = lean_ctor_get(x_17, 0); +lean_inc(x_18); +x_19 = lean_ctor_get(x_18, 0); +lean_inc(x_19); +x_20 = lean_unbox(x_19); +lean_dec(x_19); +if (x_20 == 0) +{ +lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; +x_21 = lean_ctor_get(x_17, 1); +lean_inc(x_21); +lean_dec(x_17); +x_22 = lean_ctor_get(x_18, 1); lean_inc(x_22); -x_23 = lean_ctor_get(x_22, 0); -lean_inc(x_23); -x_24 = lean_unbox(x_23); -lean_dec(x_23); -if (x_24 == 0) -{ -lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_dec(x_18); -lean_dec(x_12); -x_25 = lean_ctor_get(x_21, 1); +x_23 = lean_box(0); +x_24 = l_Lean_Elab_Tactic_evalAllGoals___lambda__1(x_22, x_23, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_21); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_24; +} +else +{ +lean_object* x_25; lean_object* x_26; uint8_t x_27; +lean_dec(x_18); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +x_25 = lean_ctor_get(x_17, 1); lean_inc(x_25); -lean_dec(x_21); -x_26 = lean_ctor_get(x_22, 1); -lean_inc(x_26); -lean_dec(x_22); -x_27 = lean_box(0); -x_28 = l_Lean_Elab_Tactic_evalAllGoals___lambda__1(x_26, x_27, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_25); -lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_3); -lean_dec(x_2); -return x_28; +lean_dec(x_17); +x_26 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg(x_25); +x_27 = !lean_is_exclusive(x_26); +if (x_27 == 0) +{ +return x_26; } else { -lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33; -lean_dec(x_22); -x_29 = lean_ctor_get(x_21, 1); +lean_object* x_28; lean_object* x_29; lean_object* x_30; +x_28 = lean_ctor_get(x_26, 0); +x_29 = lean_ctor_get(x_26, 1); lean_inc(x_29); -lean_dec(x_21); -x_30 = lean_st_ref_take(x_7, x_29); -x_31 = lean_ctor_get(x_30, 0); -lean_inc(x_31); -x_32 = lean_ctor_get(x_30, 1); -lean_inc(x_32); -lean_dec(x_30); -x_33 = !lean_is_exclusive(x_31); -if (x_33 == 0) -{ -lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; -x_34 = lean_ctor_get(x_31, 0); -lean_dec(x_34); -lean_ctor_set(x_31, 0, x_18); -x_35 = lean_st_ref_set(x_7, x_31, x_32); -x_36 = lean_ctor_get(x_35, 1); -lean_inc(x_36); -lean_dec(x_35); -x_37 = l_List_forM___at_Lean_Elab_Tactic_evalAllGoals___spec__2(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_36); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_3); -lean_dec(x_2); -if (lean_obj_tag(x_37) == 0) -{ -lean_object* x_38; lean_object* x_39; uint8_t x_40; -x_38 = lean_ctor_get(x_37, 1); -lean_inc(x_38); -lean_dec(x_37); -x_39 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg(x_38); -x_40 = !lean_is_exclusive(x_39); -if (x_40 == 0) -{ -return x_39; -} -else -{ -lean_object* x_41; lean_object* x_42; lean_object* x_43; -x_41 = lean_ctor_get(x_39, 0); -x_42 = lean_ctor_get(x_39, 1); -lean_inc(x_42); -lean_inc(x_41); -lean_dec(x_39); -x_43 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_43, 0, x_41); -lean_ctor_set(x_43, 1, x_42); -return x_43; -} -} -else -{ -uint8_t x_44; -x_44 = !lean_is_exclusive(x_37); -if (x_44 == 0) -{ -return x_37; -} -else -{ -lean_object* x_45; lean_object* x_46; lean_object* x_47; -x_45 = lean_ctor_get(x_37, 0); -x_46 = lean_ctor_get(x_37, 1); -lean_inc(x_46); -lean_inc(x_45); -lean_dec(x_37); -x_47 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_47, 0, x_45); -lean_ctor_set(x_47, 1, x_46); -return x_47; +lean_inc(x_28); +lean_dec(x_26); +x_30 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_30, 0, x_28); +lean_ctor_set(x_30, 1, x_29); +return x_30; } } } else { -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; -x_48 = lean_ctor_get(x_31, 1); -x_49 = lean_ctor_get(x_31, 2); -x_50 = lean_ctor_get(x_31, 3); -x_51 = lean_ctor_get(x_31, 4); -lean_inc(x_51); -lean_inc(x_50); -lean_inc(x_49); -lean_inc(x_48); -lean_dec(x_31); -x_52 = lean_alloc_ctor(0, 5, 0); -lean_ctor_set(x_52, 0, x_18); -lean_ctor_set(x_52, 1, x_48); -lean_ctor_set(x_52, 2, x_49); -lean_ctor_set(x_52, 3, x_50); -lean_ctor_set(x_52, 4, x_51); -x_53 = lean_st_ref_set(x_7, x_52, x_32); -x_54 = lean_ctor_get(x_53, 1); -lean_inc(x_54); -lean_dec(x_53); -x_55 = l_List_forM___at_Lean_Elab_Tactic_evalAllGoals___spec__2(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_54); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_3); -lean_dec(x_2); -if (lean_obj_tag(x_55) == 0) -{ -lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; -x_56 = lean_ctor_get(x_55, 1); -lean_inc(x_56); -lean_dec(x_55); -x_57 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg(x_56); -x_58 = lean_ctor_get(x_57, 0); -lean_inc(x_58); -x_59 = lean_ctor_get(x_57, 1); -lean_inc(x_59); -if (lean_is_exclusive(x_57)) { - lean_ctor_release(x_57, 0); - lean_ctor_release(x_57, 1); - x_60 = x_57; -} else { - lean_dec_ref(x_57); - x_60 = lean_box(0); -} -if (lean_is_scalar(x_60)) { - x_61 = lean_alloc_ctor(1, 2, 0); -} else { - x_61 = x_60; -} -lean_ctor_set(x_61, 0, x_58); -lean_ctor_set(x_61, 1, x_59); -return x_61; -} -else -{ -lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; -x_62 = lean_ctor_get(x_55, 0); -lean_inc(x_62); -x_63 = lean_ctor_get(x_55, 1); -lean_inc(x_63); -if (lean_is_exclusive(x_55)) { - lean_ctor_release(x_55, 0); - lean_ctor_release(x_55, 1); - x_64 = x_55; -} else { - lean_dec_ref(x_55); - x_64 = lean_box(0); -} -if (lean_is_scalar(x_64)) { - x_65 = lean_alloc_ctor(1, 2, 0); -} else { - x_65 = x_64; -} -lean_ctor_set(x_65, 0, x_62); -lean_ctor_set(x_65, 1, x_63); -return x_65; -} -} -} -} -else -{ -uint8_t x_66; -lean_dec(x_18); -lean_dec(x_12); +uint8_t x_31; lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); @@ -24074,23 +24075,23 @@ lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_2); -x_66 = !lean_is_exclusive(x_21); -if (x_66 == 0) +x_31 = !lean_is_exclusive(x_17); +if (x_31 == 0) { -return x_21; +return x_17; } else { -lean_object* x_67; lean_object* x_68; lean_object* x_69; -x_67 = lean_ctor_get(x_21, 0); -x_68 = lean_ctor_get(x_21, 1); -lean_inc(x_68); -lean_inc(x_67); -lean_dec(x_21); -x_69 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_69, 0, x_67); -lean_ctor_set(x_69, 1, x_68); -return x_69; +lean_object* x_32; lean_object* x_33; lean_object* x_34; +x_32 = lean_ctor_get(x_17, 0); +x_33 = lean_ctor_get(x_17, 1); +lean_inc(x_33); +lean_inc(x_32); +lean_dec(x_17); +x_34 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_34, 0, x_32); +lean_ctor_set(x_34, 1, x_33); +return x_34; } } } @@ -24124,23 +24125,11 @@ lean_dec(x_1); return x_18; } } -LEAN_EXPORT lean_object* l_List_forM___at_Lean_Elab_Tactic_evalAllGoals___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) { -_start: -{ -lean_object* x_11; -x_11 = l_List_forM___at_Lean_Elab_Tactic_evalAllGoals___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_3); -lean_dec(x_2); -return x_11; -} -} -LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___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_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); +x_9 = l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); lean_dec(x_8); lean_dec(x_7); lean_dec(x_6); @@ -49639,10 +49628,10 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_elabSetOption_declRange__1_ if (builtin) {res = l___regBuiltin_Lean_Elab_Tactic_elabSetOption_declRange__1(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -}l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__1 = _init_l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__1(); -lean_mark_persistent(l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__1); -l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__2 = _init_l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__2(); -lean_mark_persistent(l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__3___rarg___closed__2); +}l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__1 = _init_l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__1(); +lean_mark_persistent(l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__1); +l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__2 = _init_l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__2(); +lean_mark_persistent(l_Lean_Elab_throwAbortTactic___at_Lean_Elab_Tactic_evalAllGoals___spec__2___rarg___closed__2); l_Lean_Elab_Tactic_evalAllGoals___closed__1 = _init_l_Lean_Elab_Tactic_evalAllGoals___closed__1(); lean_mark_persistent(l_Lean_Elab_Tactic_evalAllGoals___closed__1); l___regBuiltin_Lean_Elab_Tactic_evalAllGoals__1___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalAllGoals__1___closed__1(); diff --git a/stage0/stdlib/Lean/Elab/Tactic/Induction.c b/stage0/stdlib/Lean/Elab/Tactic/Induction.c index 0ed786224f..9d705cc230 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/Induction.c +++ b/stage0/stdlib/Lean/Elab/Tactic/Induction.c @@ -25,11 +25,10 @@ LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_Elim static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___lambda__1___closed__4; LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_withAltsOfOptInductionAlts___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__11; static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___lambda__1___closed__1; LEAN_EXPORT lean_object* l_Lean_PersistentArray_mapMAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__2; static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__8___closed__5; -LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1(lean_object*, size_t, size_t, lean_object*); static lean_object* l_Lean_Elab_Tactic_elabElimTargets___lambda__1___closed__6; lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___boxed(lean_object*); @@ -38,6 +37,7 @@ lean_object* l_Lean_Meta_getElimExprInfo(lean_object*, lean_object*, lean_object LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_format_pretty(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_elabElimTargets___lambda__1___closed__3; +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993_(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___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___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName(lean_object*); LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___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*); @@ -50,6 +50,7 @@ static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induc LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt___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_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_ElimApp_mkElimApp___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS(lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_LocalContext_getFVars___spec__1(size_t, size_t, lean_object*); static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___closed__10; lean_object* l_Lean_Elab_Term_resolveId_x3f(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -59,7 +60,6 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Tactic_ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange__1___closed__1; LEAN_EXPORT lean_object* l_panic___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_throwTacticEx___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__12; lean_object* lean_mk_empty_array_with_capacity(lean_object*); lean_object* l_Lean_mkAppN(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapFinIdxM_map___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -70,22 +70,18 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSa LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getArgExpectedType(lean_object*); static lean_object* l_Lean_Elab_Tactic_mkTargetView___lambda__2___closed__1; static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_withAltsOfOptInductionAlts___rarg___lambda__1___closed__1; -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt___boxed(lean_object*); static lean_object* l_Lean_Elab_Tactic_elabFunTargetCall___lambda__2___closed__4; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__1___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_List_mapTR_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__4(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_checkInductionTargets___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__4; static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___closed__11; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInduction__1___closed__2; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_elabFunTargetCall___closed__4; -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__2; static lean_object* l_Array_zipWithAux___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___spec__2___lambda__1___closed__6; static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__8___closed__3; LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_elabElimTargets___spec__8(lean_object*, size_t, size_t, lean_object*); -static lean_object* l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_checkInductionTargets___spec__1___at_Lean_Elab_Tactic_checkInductionTargets___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___lambda__3(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*); static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___closed__2; @@ -100,11 +96,12 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambd LEAN_EXPORT lean_object* l_Lean_Elab_Term_withNarrowedTacticReuse___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_withAltsOfOptInductionAlts___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__5___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__6___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_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_shouldExpandAlt___boxed(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f(lean_object*); static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___lambda__5___closed__1; +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__5; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_evalInductionCore(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_elabElimTargets___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_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(lean_object*); static lean_object* l_Lean_Elab_Tactic_elabFunTargetCall___closed__1; static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_evalInductionCore___lambda__4___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp_loop___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -117,7 +114,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___boxed( static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__6___closed__2; lean_object* l_Lean_Syntax_formatStxAux(lean_object*, uint8_t, 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_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInduction_declRange__1___closed__2; LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalTacticAt(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -127,6 +123,7 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFunInduction__1(lea LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabFunTargetCall(uint8_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_evalCases___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCasesCore___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandAlt_x3f(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp_loop___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_evalInductionCore___lambda__1___boxed(lean_object**); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___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*); @@ -140,18 +137,14 @@ lean_object* l_Lean_Expr_sort___override(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_withoutErrToSorry___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabTermForElim___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___lambda__2___closed__3; lean_object* l_Lean_MessageData_ofList(lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__5; static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__5; static lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__2___closed__3; lean_object* lean_array_push(lean_object*, lean_object*); lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange__1___closed__7; -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__13; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___spec__1___boxed(lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__14; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltVars___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabElimTargets(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__1; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInduction_declRange__1___closed__6; static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___lambda__3___closed__2; static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___closed__7; @@ -171,6 +164,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_ static lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__1___closed__1; lean_object* lean_mk_array(lean_object*, lean_object*); lean_object* l_Lean_MVarId_assign___at_Lean_Elab_Tactic_refineCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__10; LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFunCases__1(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___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*); @@ -198,8 +192,8 @@ static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induc lean_object* l_Lean_MVarId_setKind(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts___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_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltRHS(lean_object*); +LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandAlt_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_withReuseContext___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_evalInductionCore___spec__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_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__6; lean_object* l_Lean_addBuiltinDeclarationRanges(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___closed__8; lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*, uint8_t); @@ -212,6 +206,7 @@ static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induc LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__5___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__6___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFunInduction__2(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getNumExplicitFields___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__3; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_evalInductionCore___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___lambda__3(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_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_addNewArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -221,14 +216,11 @@ 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*); static lean_object* l_Std_Range_forIn_x27_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__4___lambda__1___closed__3; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__1(size_t, size_t, lean_object*); -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_withAltsOfOptInductionAlts___rarg___lambda__1___boxed(lean_object*); static lean_object* l_Std_Range_forIn_x27_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__4___closed__1; lean_object* l_Lean_stringToMessageData(lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__10; lean_object* l_Lean_Expr_mvar___override(lean_object*); LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_elabElimTargets___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__3; LEAN_EXPORT lean_object* l_Lean_Elab_Term_withNarrowedTacticReuse___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_evalInductionCore___spec__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_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts___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_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -267,6 +259,7 @@ LEAN_EXPORT uint8_t l_Lean_Elab_Tactic_isHoleRHS(lean_object*); static lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__2___closed__11; static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_inductionAltsPos___closed__6; LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__4___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__3; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalFunCases(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Array_contains___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit___spec__3(lean_object*, lean_object*); uint8_t l_Lean_Expr_isType(lean_object*); @@ -301,6 +294,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambd lean_object* l_List_appendTR___rarg(lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_ElimApp_setMotiveArg___closed__4; lean_object* l_Lean_Elab_Term_withoutHeedElabAsElimImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__4; static lean_object* l_panic___at_Lean_Elab_Tactic_elabElimTargets___spec__9___closed__1; LEAN_EXPORT lean_object* l_Array_filterMapM___at_Lean_Elab_Tactic_elabElimTargets___spec__4(lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_isWildcard(lean_object*); @@ -312,6 +306,7 @@ size_t lean_usize_of_nat(lean_object*); static lean_object* l_Std_Range_forIn_x27_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__4___lambda__1___closed__1; lean_object* l_Lean_Elab_Tactic_getNameOfIdent_x27(lean_object*); lean_object* l_Lean_Elab_Tactic_getGoals___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__2; static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___closed__3; lean_object* l_Lean_Elab_Tactic_getUnsolvedGoals(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_evalFunCases__1___closed__2; @@ -352,8 +347,6 @@ LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_T static lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp___closed__1; LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_ElimApp_mkElimApp_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_zip___rarg(lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__1; -LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890_(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_mkTargetView___lambda__2(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_Term_withoutTacticIncrementality___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac___spec__1___closed__2; LEAN_EXPORT lean_object* l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -374,7 +367,6 @@ lean_object* l_Lean_MVarId_getType(lean_object*, lean_object*, lean_object*, lea LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___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* l_Lean_Elab_Term_withoutErrToSorryImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___lambda__3___closed__1; -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__6; static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___lambda__2___closed__10; static lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__2___closed__4; LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -403,6 +395,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tac static lean_object* l_Lean_Elab_Tactic_elabFunTargetCall___closed__7; uint8_t l_Lean_InductiveVal_isNested(lean_object*); lean_object* l_Lean_addTrace___at_Lean_Elab_Tactic_evalTactic_handleEx___spec__2(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_evalAlt___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* l_Lean_Syntax_getKind(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalFunInduction___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Std_Range_forIn_x27_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental___spec__4___lambda__1(lean_object*, lean_object*); @@ -416,6 +409,7 @@ lean_object* l_Lean_MVarId_withContext___at___private_Lean_Meta_SynthInstance_0_ static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___lambda__3___closed__6; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_elabFunTargetCall___closed__8; +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__1; LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___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_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget(uint8_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___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltVars(lean_object*); @@ -433,7 +427,6 @@ static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_g static lean_object* l_Lean_Elab_Tactic_elabFunTargetCall___closed__10; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_whnfForall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__7; LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_ref_get(lean_object*, lean_object*); @@ -460,6 +453,7 @@ static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_E lean_object* l_Lean_Meta_abstractMVars(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCasesCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__12; LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental___spec__8___lambda__2(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*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___closed__8; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -484,10 +478,9 @@ LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_T LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__2___closed__9; extern lean_object* l_Lean_instInhabitedExpr; -LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_InfoTree_substitute(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__8; LEAN_EXPORT lean_object* l_Lean_Elab_Term_withNarrowedArgTacticReuse___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_evalInductionCore___spec__1___lambda__1___boxed(lean_object*, lean_object*); lean_object* l_Lean_Meta_addImplicitTargets(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_constName_x3f(lean_object*); @@ -496,6 +489,7 @@ static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_E static lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__2___closed__5; static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_withAltsOfOptInductionAlts___rarg___lambda__2___closed__1; static lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp___closed__2; +static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__1; LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInduction_declRange__1___closed__3; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabFunTargetCall___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*); @@ -513,6 +507,7 @@ extern lean_object* l_Task_Priority_default; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_checkInductionTargets___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___lambda__3___closed__3; static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___lambda__2___closed__13; +LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandAlt_x3f___spec__1(lean_object*, size_t, size_t, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_withNarrowedTacticReuse___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_withAltsOfOptInductionAlts___spec__1___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_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental___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* l_Lean_Meta_mkFreshBinderNameForTactic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -547,20 +542,21 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tac static lean_object* l_Lean_Elab_Tactic_elabElimTargets___lambda__1___closed__5; lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_saveState___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__15; uint8_t l_Lean_Syntax_isIdent(lean_object*); -LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427_(lean_object*); static lean_object* l_Lean_Elab_Term_withoutTacticIncrementality___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac___spec__1___closed__3; static lean_object* l_Lean_Elab_Tactic_elabFunTargetCall___closed__5; static lean_object* l_Lean_Elab_Tactic_elabElimTargets___lambda__1___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_addConstInfo___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Tactic_evalTactic_eval___spec__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_elabFunTargetCall___lambda__2___closed__1; +static lean_object* l_Lean_Elab_Tactic_evalAlt___closed__1; extern lean_object* l_Lean_Language_Snapshot_Diagnostics_empty; static lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__2___closed__7; static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___lambda__4___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__7___boxed(lean_object**); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__6; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___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*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__11; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_eraseIdx___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltLhses___boxed(lean_object*); @@ -569,7 +565,6 @@ static lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp_loop___closed__2; extern lean_object* l_Std_Format_defWidth; static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___lambda__1___closed__1; static lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___lambda__2___closed__4; -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__5; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange__1___closed__4; extern lean_object* l_Lean_Meta_instInhabitedElimAltInfo; LEAN_EXPORT lean_object* l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -643,6 +638,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_withNarrowedTacticReuse___at___private static lean_object* l_Lean_Elab_Tactic_isHoleRHS___closed__1; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___spec__1(size_t, size_t, lean_object*); static lean_object* l_Lean_Elab_Tactic_ElimApp_instInhabitedAlt___closed__2; +lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_inductionAltsPos___closed__4; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getArgExpectedType___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental___spec__8___boxed(lean_object**); @@ -661,20 +657,21 @@ LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_ static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__8___closed__6; static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__8___closed__1; extern lean_object* l_Lean_NameSet_empty; +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__5; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getFType___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabTermForElim___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_mkTargetView(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_evalInduction___lambda__2(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_elabFunTargetCall___closed__12; -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__3; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getArgExpectedType___boxed(lean_object*); LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_app___override(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_withNarrowedTacticReuse___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_evalInductionCore___spec__2___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*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__4; +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__7; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCases__1___closed__3; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__6___boxed(lean_object**); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__14; uint8_t lean_nat_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_MVarId_getDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_elabElimTargets___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -682,9 +679,11 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInduction__2(lean_o lean_object* l_Lean_Elab_getResetInfoTrees___at_Lean_Elab_Term_withDeclName___spec__3___rarg(lean_object*, lean_object*); static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___lambda__2___closed__2; lean_object* l_Lean_Language_SnapshotTask_cancelRec___rarg(lean_object*, lean_object*, lean_object*); +static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltDArrow(lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_evalAlt___closed__2; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getOptPreTacOfOptInductionAlts(lean_object*); lean_object* l_Lean_MessageData_ofLevel(lean_object*); LEAN_EXPORT uint8_t l_Std_Range_forIn_x27_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__4___lambda__2(lean_object*); @@ -697,7 +696,6 @@ static lean_object* l_Lean_Elab_Tactic_mkTargetView___closed__3; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_mkTargetView___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_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_ElimApp_mkElimApp___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_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__2; lean_object* l_Lean_indentExpr(lean_object*); uint8_t l_Lean_BinderInfo_isExplicit(uint8_t); lean_object* l_Lean_Meta_getMVarsNoDelayed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -708,6 +706,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental__ lean_object* l_Lean_Meta_getFVarSetToGeneralize(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabFunTargetCall___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*); static lean_object* l_Lean_Elab_Tactic_ElimApp_setMotiveArg___closed__6; +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__9; static lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental___spec__8___lambda__2___closed__1; lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Tactic_evalTactic___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___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*); @@ -734,7 +733,6 @@ lean_object* lean_panic_fn(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___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*); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__1; LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___lambda__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___boxed__const__1; @@ -746,13 +744,13 @@ lean_object* l_Lean_MVarId_tryClear(lean_object*, lean_object*, lean_object*, le lean_object* l_Lean_Expr_getAppFn(lean_object*); uint8_t l_Lean_Expr_isProp(lean_object*); LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__5___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Term_withNarrowedTacticReuse___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_withAltsOfOptInductionAlts___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getOptPreTacOfOptInductionAlts___boxed(lean_object*); static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___closed__1; LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_checkInductionTargets___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts___lambda__1___boxed(lean_object**); -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__9; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___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_ElimApp_evalAlts___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapFinIdxM_map___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -770,6 +768,7 @@ LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___at_Lean_Elab_Tactic_ElimAp LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__1(lean_object*, size_t, size_t); lean_object* l_Lean_RBNode_insert___at_Lean_FVarIdSet_insert___spec__1(lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange__1___closed__5; +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__8; static lean_object* l_Std_Range_forIn_x27_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithIncremental___spec__4___closed__3; static lean_object* l_Lean_Elab_Tactic_mkTargetView___closed__6; LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -795,6 +794,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___boxed static lean_object* l_Lean_Elab_Tactic_mkTargetView___closed__4; LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__5___boxed(lean_object**); size_t lean_usize_add(size_t, size_t); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__15; static lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp_loop___closed__4; static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__8___closed__7; static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___lambda__6___closed__4; @@ -818,10 +818,12 @@ static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induc lean_object* l_Lean_Language_SnapshotTask_get___rarg(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabFunTargetCall___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInduction__1(lean_object*); lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); uint8_t l_Lean_isInductiveCore(lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__6; LEAN_EXPORT lean_object* l_Lean_Elab_Term_withNarrowedArgTacticReuse___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_evalInductionCore___spec__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*); static lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___closed__2; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_setMotiveArg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -831,6 +833,7 @@ lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_o static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_inductionAltsPos___closed__2; lean_object* l_Lean_Expr_bindingBody_x21(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInduction_x3f(lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__4; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange__1___closed__2; static lean_object* l_Std_Range_forIn_x27_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__4___lambda__1___closed__2; lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*); @@ -860,6 +863,7 @@ lean_object* l_Lean_throwError___at_Lean_Meta_mkSimpCongrTheorem___spec__6(lean_ LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getFirstAltLhs___boxed(lean_object*); lean_object* lean_array_get_size(lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___spec__11(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__13; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___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*); static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___lambda__2___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabElimTargets___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*); @@ -875,6 +879,7 @@ static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induc static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_withAltsOfOptInductionAlts___rarg___lambda__1___closed__2; static size_t l_Array_zipWithAux___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___spec__2___lambda__1___closed__3; lean_object* l_Lean_Elab_admitGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456_(lean_object*); lean_object* l_Lean_Meta_Cases_unifyEqs_x3f(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_withSaveInfoContext___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp_loop___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*); @@ -904,6 +909,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__2 LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___lambda__1___boxed(lean_object**); static lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__2___closed__8; static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__7; +LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_shouldExpandAlt(lean_object*); static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___closed__10; uint8_t l_Lean_Expr_isFVar(lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___spec__7(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -945,7 +951,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tac LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds(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_ElimApp_mkElimApp_loop___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*); static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange__1___closed__3; -LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt___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_evalAlt___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyAltStx___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getFType___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___closed__2; @@ -1196,13 +1202,86 @@ lean_dec(x_1); return x_2; } } +static lean_object* _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_unchecked("null", 4, 4); +return x_1; +} +} +static lean_object* _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__1; +x_3 = l_Lean_Name_str___override(x_1, x_2); +return x_3; +} +} +LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; +x_2 = lean_unsigned_to_nat(1u); +x_3 = l_Lean_Syntax_getArg(x_1, x_2); +x_4 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; +lean_inc(x_3); +x_5 = l_Lean_Syntax_isOfKind(x_3, x_4); +if (x_5 == 0) +{ +uint8_t x_6; +lean_dec(x_3); +x_6 = 1; +return x_6; +} +else +{ +lean_object* x_7; lean_object* x_8; uint8_t x_9; +x_7 = l_Lean_Syntax_getNumArgs(x_3); +lean_dec(x_3); +x_8 = lean_unsigned_to_nat(0u); +x_9 = lean_nat_dec_lt(x_8, x_7); +lean_dec(x_7); +return x_9; +} +} +} +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___boxed(lean_object* x_1) { +_start: +{ +uint8_t x_2; lean_object* x_3; +x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS(x_1); +lean_dec(x_1); +x_3 = lean_box(x_2); +return x_3; +} +} LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltRHS(lean_object* x_1) { _start: { -lean_object* x_2; lean_object* x_3; -x_2 = lean_unsigned_to_nat(2u); +lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; +x_2 = lean_unsigned_to_nat(1u); x_3 = l_Lean_Syntax_getArg(x_1, x_2); -return x_3; +x_4 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; +lean_inc(x_3); +x_5 = l_Lean_Syntax_isOfKind(x_3, x_4); +if (x_5 == 0) +{ +lean_object* x_6; lean_object* x_7; +lean_dec(x_3); +x_6 = lean_unsigned_to_nat(2u); +x_7 = l_Lean_Syntax_getArg(x_1, x_6); +return x_7; +} +else +{ +lean_object* x_8; +x_8 = l_Lean_Syntax_getArg(x_3, x_2); +lean_dec(x_3); +return x_8; +} } } LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltRHS___boxed(lean_object* x_1) { @@ -1217,11 +1296,25 @@ return x_2; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltDArrow(lean_object* x_1) { _start: { -lean_object* x_2; lean_object* x_3; +lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; x_2 = lean_unsigned_to_nat(1u); x_3 = l_Lean_Syntax_getArg(x_1, x_2); +x_4 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; +lean_inc(x_3); +x_5 = l_Lean_Syntax_isOfKind(x_3, x_4); +if (x_5 == 0) +{ return x_3; } +else +{ +lean_object* x_6; lean_object* x_7; +x_6 = lean_unsigned_to_nat(0u); +x_7 = l_Lean_Syntax_getArg(x_3, x_6); +lean_dec(x_3); +return x_7; +} +} } LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltDArrow___boxed(lean_object* x_1) { _start: @@ -1284,24 +1377,6 @@ x_3 = lean_box(x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__1() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string_unchecked("null", 4, 4); -return x_1; -} -} -static lean_object* _init_l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__1; -x_3 = l_Lean_Name_str___override(x_1, x_2); -return x_3; -} -} LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___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, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) { _start: { @@ -1315,7 +1390,7 @@ lean_ctor_set(x_15, 0, x_1); lean_ctor_set(x_15, 1, x_14); x_16 = lean_array_mk(x_15); x_17 = lean_box(2); -x_18 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_18 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_19 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_19, 0, x_17); lean_ctor_set(x_19, 1, x_18); @@ -1474,7 +1549,7 @@ lean_ctor_set(x_26, 0, x_25); lean_ctor_set(x_26, 1, x_20); x_27 = lean_array_mk(x_26); x_28 = lean_box(2); -x_29 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_29 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_30 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_30, 0, x_28); lean_ctor_set(x_30, 1, x_29); @@ -1588,7 +1663,7 @@ lean_ctor_set(x_52, 0, x_50); lean_ctor_set(x_52, 1, x_51); x_53 = lean_array_mk(x_52); x_54 = lean_box(2); -x_55 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_55 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_56 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_56, 0, x_54); lean_ctor_set(x_56, 1, x_55); @@ -1721,7 +1796,7 @@ lean_ctor_set(x_82, 0, x_80); lean_ctor_set(x_82, 1, x_81); x_83 = lean_array_mk(x_82); x_84 = lean_box(2); -x_85 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_85 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_86 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_86, 0, x_84); lean_ctor_set(x_86, 1, x_85); @@ -1835,25 +1910,26 @@ x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt___lambda__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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) { +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt___lambda__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, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) { _start: { -lean_object* x_12; +lean_object* x_13; lean_inc(x_1); -x_12 = l_Lean_MVarId_getDecl(x_1, x_7, x_8, x_9, x_10, x_11); -if (lean_obj_tag(x_12) == 0) +x_13 = l_Lean_MVarId_getDecl(x_1, x_8, x_9, x_10, x_11, x_12); +if (lean_obj_tag(x_13) == 0) { -lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18; -x_13 = lean_ctor_get(x_12, 0); -lean_inc(x_13); -x_14 = lean_ctor_get(x_12, 1); +lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; +x_14 = lean_ctor_get(x_13, 0); lean_inc(x_14); -lean_dec(x_12); -x_15 = lean_ctor_get(x_13, 2); +x_15 = lean_ctor_get(x_13, 1); lean_inc(x_15); -x_16 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_16, 0, x_15); -x_17 = 0; +lean_dec(x_13); +x_16 = lean_ctor_get(x_14, 2); +lean_inc(x_16); +x_17 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_17, 0, x_16); +x_18 = 0; +lean_inc(x_11); lean_inc(x_10); lean_inc(x_9); lean_inc(x_8); @@ -1861,45 +1937,39 @@ lean_inc(x_7); lean_inc(x_6); lean_inc(x_5); lean_inc(x_4); -lean_inc(x_3); -x_18 = l_Lean_Elab_Tactic_elabTermEnsuringType(x_2, x_16, x_17, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_14); -if (lean_obj_tag(x_18) == 0) +x_19 = l_Lean_Elab_Tactic_elabTermEnsuringType(x_2, x_17, x_18, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_15); +if (lean_obj_tag(x_19) == 0) { -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; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; -x_19 = lean_ctor_get(x_18, 0); -lean_inc(x_19); -x_20 = lean_ctor_get(x_18, 1); +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; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; +x_20 = lean_ctor_get(x_19, 0); lean_inc(x_20); -lean_dec(x_18); -lean_inc(x_19); -x_21 = l_Lean_MVarId_assign___at_Lean_Elab_Tactic_refineCore___spec__1(x_1, x_19, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_20); -x_22 = lean_ctor_get(x_21, 1); -lean_inc(x_22); -lean_dec(x_21); -x_23 = l_Lean_Meta_getMVarsNoDelayed(x_19, x_7, x_8, x_9, x_10, x_22); -x_24 = lean_ctor_get(x_23, 0); -lean_inc(x_24); -x_25 = lean_ctor_get(x_23, 1); +x_21 = lean_ctor_get(x_19, 1); +lean_inc(x_21); +lean_dec(x_19); +lean_inc(x_20); +x_22 = l_Lean_MVarId_assign___at_Lean_Elab_Tactic_refineCore___spec__1(x_1, x_20, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_21); +x_23 = lean_ctor_get(x_22, 1); +lean_inc(x_23); +lean_dec(x_22); +x_24 = l_Lean_Meta_getMVarsNoDelayed(x_20, x_8, x_9, x_10, x_11, x_23); +x_25 = lean_ctor_get(x_24, 0); lean_inc(x_25); -lean_dec(x_23); -x_26 = lean_ctor_get(x_13, 0); +x_26 = lean_ctor_get(x_24, 1); lean_inc(x_26); -lean_dec(x_13); -x_27 = lean_array_to_list(x_24); -x_28 = l_Lean_Elab_Tactic_evalAlt___lambda__3___closed__2; +lean_dec(x_24); +x_27 = lean_ctor_get(x_14, 0); lean_inc(x_27); -x_29 = l_Lean_Elab_Tactic_tagUntaggedGoals(x_26, x_28, x_27, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_25); -x_30 = lean_ctor_get(x_29, 1); -lean_inc(x_30); -lean_dec(x_29); -x_31 = l_Lean_Elab_Tactic_getGoals___rarg(x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_30); -x_32 = lean_ctor_get(x_31, 0); -lean_inc(x_32); -x_33 = lean_ctor_get(x_31, 1); -lean_inc(x_33); -lean_dec(x_31); -x_34 = l_List_appendTR___rarg(x_32, x_27); -x_35 = l_Lean_Elab_Tactic_setGoals(x_34, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_33); +lean_dec(x_14); +x_28 = lean_array_to_list(x_25); +x_29 = l_Lean_Elab_Tactic_evalAlt___lambda__3___closed__2; +lean_inc(x_28); +x_30 = l_Lean_Elab_Tactic_tagUntaggedGoals(x_27, x_29, x_28, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_26); +x_31 = lean_ctor_get(x_30, 1); +lean_inc(x_31); +lean_dec(x_30); +x_32 = l_List_appendTR___rarg(x_3, x_28); +x_33 = l_Lean_Elab_Tactic_setGoals(x_32, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_31); +lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); @@ -1907,13 +1977,13 @@ lean_dec(x_7); lean_dec(x_6); lean_dec(x_5); lean_dec(x_4); -lean_dec(x_3); -return x_35; +return x_33; } else { -uint8_t x_36; -lean_dec(x_13); +uint8_t x_34; +lean_dec(x_14); +lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); @@ -1923,91 +1993,29 @@ lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_1); -x_36 = !lean_is_exclusive(x_18); -if (x_36 == 0) +x_34 = !lean_is_exclusive(x_19); +if (x_34 == 0) { -return x_18; +return x_19; } else { -lean_object* x_37; lean_object* x_38; lean_object* x_39; -x_37 = lean_ctor_get(x_18, 0); -x_38 = lean_ctor_get(x_18, 1); -lean_inc(x_38); -lean_inc(x_37); -lean_dec(x_18); -x_39 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_39, 0, x_37); -lean_ctor_set(x_39, 1, x_38); -return x_39; +lean_object* x_35; lean_object* x_36; lean_object* x_37; +x_35 = lean_ctor_get(x_19, 0); +x_36 = lean_ctor_get(x_19, 1); +lean_inc(x_36); +lean_inc(x_35); +lean_dec(x_19); +x_37 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_37, 0, x_35); +lean_ctor_set(x_37, 1, x_36); +return x_37; } } } else { -uint8_t x_40; -lean_dec(x_10); -lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_5); -lean_dec(x_4); -lean_dec(x_3); -lean_dec(x_2); -lean_dec(x_1); -x_40 = !lean_is_exclusive(x_12); -if (x_40 == 0) -{ -return x_12; -} -else -{ -lean_object* x_41; lean_object* x_42; lean_object* x_43; -x_41 = lean_ctor_get(x_12, 0); -x_42 = lean_ctor_get(x_12, 1); -lean_inc(x_42); -lean_inc(x_41); -lean_dec(x_12); -x_43 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_43, 0, x_41); -lean_ctor_set(x_43, 1, x_42); -return x_43; -} -} -} -} -LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt___lambda__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, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) { -_start: -{ -lean_object* x_13; -lean_inc(x_11); -lean_inc(x_10); -lean_inc(x_9); -lean_inc(x_8); -lean_inc(x_7); -lean_inc(x_6); -x_13 = lean_apply_7(x_1, x_6, x_7, x_8, x_9, x_10, x_11, x_12); -if (lean_obj_tag(x_13) == 0) -{ -lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; -x_14 = lean_ctor_get(x_13, 1); -lean_inc(x_14); -lean_dec(x_13); -lean_inc(x_3); -lean_inc(x_2); -x_15 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__3), 11, 2); -lean_closure_set(x_15, 0, x_2); -lean_closure_set(x_15, 1, x_3); -x_16 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_withTacticInfoContext___rarg), 11, 2); -lean_closure_set(x_16, 0, x_3); -lean_closure_set(x_16, 1, x_15); -x_17 = l_Lean_MVarId_withContext___at_Lean_Elab_Tactic_withMainContext___spec__1___rarg(x_2, x_16, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_14); -return x_17; -} -else -{ -uint8_t x_18; +uint8_t x_38; lean_dec(x_11); lean_dec(x_10); lean_dec(x_9); @@ -2018,62 +2026,289 @@ lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_2); -x_18 = !lean_is_exclusive(x_13); -if (x_18 == 0) +lean_dec(x_1); +x_38 = !lean_is_exclusive(x_13); +if (x_38 == 0) { return x_13; } else { -lean_object* x_19; lean_object* x_20; lean_object* x_21; -x_19 = lean_ctor_get(x_13, 0); -x_20 = lean_ctor_get(x_13, 1); -lean_inc(x_20); -lean_inc(x_19); +lean_object* x_39; lean_object* x_40; lean_object* x_41; +x_39 = lean_ctor_get(x_13, 0); +x_40 = lean_ctor_get(x_13, 1); +lean_inc(x_40); +lean_inc(x_39); lean_dec(x_13); -x_21 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_21, 0, x_19); +x_41 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_41, 0, x_39); +lean_ctor_set(x_41, 1, x_40); +return x_41; +} +} +} +} +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt___lambda__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, 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) { +_start: +{ +lean_object* x_14; +lean_inc(x_12); +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +x_14 = lean_apply_7(x_1, x_7, x_8, x_9, x_10, x_11, x_12, x_13); +if (lean_obj_tag(x_14) == 0) +{ +lean_object* x_15; lean_object* x_16; uint8_t x_17; +x_15 = lean_ctor_get(x_14, 1); +lean_inc(x_15); +lean_dec(x_14); +x_16 = l_Lean_Elab_Tactic_getGoals___rarg(x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_15); +x_17 = !lean_is_exclusive(x_16); +if (x_17 == 0) +{ +lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; +x_18 = lean_ctor_get(x_16, 0); +x_19 = lean_ctor_get(x_16, 1); +x_20 = lean_box(0); +lean_inc(x_2); +lean_ctor_set_tag(x_16, 1); +lean_ctor_set(x_16, 1, x_20); +lean_ctor_set(x_16, 0, x_2); +x_21 = l_Lean_Elab_Tactic_setGoals(x_16, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_19); +x_22 = !lean_is_exclusive(x_21); +if (x_22 == 0) +{ +lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; +x_23 = lean_ctor_get(x_21, 1); +x_24 = lean_ctor_get(x_21, 0); +lean_dec(x_24); +x_25 = lean_unsigned_to_nat(0u); +x_26 = l_Lean_Syntax_getArg(x_3, x_25); +lean_inc(x_4); +lean_ctor_set_tag(x_21, 1); lean_ctor_set(x_21, 1, x_20); -return x_21; +lean_ctor_set(x_21, 0, x_4); +x_27 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_27, 0, x_26); +lean_ctor_set(x_27, 1, x_21); +x_28 = lean_array_mk(x_27); +x_29 = lean_box(2); +x_30 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; +x_31 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_31, 0, x_29); +lean_ctor_set(x_31, 1, x_30); +lean_ctor_set(x_31, 2, x_28); +lean_inc(x_2); +x_32 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__3), 12, 3); +lean_closure_set(x_32, 0, x_2); +lean_closure_set(x_32, 1, x_4); +lean_closure_set(x_32, 2, x_18); +x_33 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_withTacticInfoContext___rarg), 11, 2); +lean_closure_set(x_33, 0, x_31); +lean_closure_set(x_33, 1, x_32); +x_34 = l_Lean_MVarId_withContext___at_Lean_Elab_Tactic_withMainContext___spec__1___rarg(x_2, x_33, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_23); +return x_34; +} +else +{ +lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* 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; +x_35 = lean_ctor_get(x_21, 1); +lean_inc(x_35); +lean_dec(x_21); +x_36 = lean_unsigned_to_nat(0u); +x_37 = l_Lean_Syntax_getArg(x_3, x_36); +lean_inc(x_4); +x_38 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_38, 0, x_4); +lean_ctor_set(x_38, 1, x_20); +x_39 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_39, 0, x_37); +lean_ctor_set(x_39, 1, x_38); +x_40 = lean_array_mk(x_39); +x_41 = lean_box(2); +x_42 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; +x_43 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_43, 0, x_41); +lean_ctor_set(x_43, 1, x_42); +lean_ctor_set(x_43, 2, x_40); +lean_inc(x_2); +x_44 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__3), 12, 3); +lean_closure_set(x_44, 0, x_2); +lean_closure_set(x_44, 1, x_4); +lean_closure_set(x_44, 2, x_18); +x_45 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_withTacticInfoContext___rarg), 11, 2); +lean_closure_set(x_45, 0, x_43); +lean_closure_set(x_45, 1, x_44); +x_46 = l_Lean_MVarId_withContext___at_Lean_Elab_Tactic_withMainContext___spec__1___rarg(x_2, x_45, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_35); +return x_46; } } +else +{ +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_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; +x_47 = lean_ctor_get(x_16, 0); +x_48 = lean_ctor_get(x_16, 1); +lean_inc(x_48); +lean_inc(x_47); +lean_dec(x_16); +x_49 = lean_box(0); +lean_inc(x_2); +x_50 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_50, 0, x_2); +lean_ctor_set(x_50, 1, x_49); +x_51 = l_Lean_Elab_Tactic_setGoals(x_50, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_48); +x_52 = lean_ctor_get(x_51, 1); +lean_inc(x_52); +if (lean_is_exclusive(x_51)) { + lean_ctor_release(x_51, 0); + lean_ctor_release(x_51, 1); + x_53 = x_51; +} else { + lean_dec_ref(x_51); + x_53 = lean_box(0); +} +x_54 = lean_unsigned_to_nat(0u); +x_55 = l_Lean_Syntax_getArg(x_3, x_54); +lean_inc(x_4); +if (lean_is_scalar(x_53)) { + x_56 = lean_alloc_ctor(1, 2, 0); +} else { + x_56 = x_53; + lean_ctor_set_tag(x_56, 1); +} +lean_ctor_set(x_56, 0, x_4); +lean_ctor_set(x_56, 1, x_49); +x_57 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_57, 0, x_55); +lean_ctor_set(x_57, 1, x_56); +x_58 = lean_array_mk(x_57); +x_59 = lean_box(2); +x_60 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; +x_61 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_61, 0, x_59); +lean_ctor_set(x_61, 1, x_60); +lean_ctor_set(x_61, 2, x_58); +lean_inc(x_2); +x_62 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__3), 12, 3); +lean_closure_set(x_62, 0, x_2); +lean_closure_set(x_62, 1, x_4); +lean_closure_set(x_62, 2, x_47); +x_63 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_withTacticInfoContext___rarg), 11, 2); +lean_closure_set(x_63, 0, x_61); +lean_closure_set(x_63, 1, x_62); +x_64 = l_Lean_MVarId_withContext___at_Lean_Elab_Tactic_withMainContext___spec__1___rarg(x_2, x_63, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_52); +return x_64; +} +} +else +{ +uint8_t x_65; +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_2); +x_65 = !lean_is_exclusive(x_14); +if (x_65 == 0) +{ +return x_14; +} +else +{ +lean_object* x_66; lean_object* x_67; lean_object* x_68; +x_66 = lean_ctor_get(x_14, 0); +x_67 = lean_ctor_get(x_14, 1); +lean_inc(x_67); +lean_inc(x_66); +lean_dec(x_14); +x_68 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_68, 0, x_66); +lean_ctor_set(x_68, 1, x_67); +return x_68; +} +} +} +} +static lean_object* _init_l_Lean_Elab_Tactic_evalAlt___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_unchecked("(internal error) RHS was not expanded", 37, 37); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Tactic_evalAlt___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Elab_Tactic_evalAlt___closed__1; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; } } LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) { _start: { -lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; -x_13 = lean_unsigned_to_nat(2u); -x_14 = l_Lean_Syntax_getArg(x_2, x_13); -x_15 = lean_unsigned_to_nat(1u); -x_16 = l_Lean_Syntax_getArg(x_2, x_15); -lean_inc(x_14); -x_17 = l_Lean_Elab_Tactic_isHoleRHS(x_14); -if (x_17 == 0) +uint8_t x_13; +x_13 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS(x_2); +if (x_13 == 0) { -lean_object* x_18; lean_object* x_19; -lean_inc(x_14); -lean_inc(x_16); -x_18 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__2___boxed), 14, 5); -lean_closure_set(x_18, 0, x_1); -lean_closure_set(x_18, 1, x_2); -lean_closure_set(x_18, 2, x_16); -lean_closure_set(x_18, 3, x_3); -lean_closure_set(x_18, 4, x_14); -x_19 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1(x_16, x_14, x_18, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); -return x_19; +lean_object* x_14; lean_object* x_15; +lean_dec(x_3); +lean_dec(x_1); +x_14 = l_Lean_Elab_Tactic_evalAlt___closed__2; +x_15 = l_Lean_throwErrorAt___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__1(x_2, x_14, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); +lean_dec(x_11); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_2); +return x_15; } else { -lean_object* x_20; lean_object* x_21; -lean_dec(x_2); -lean_inc(x_14); -x_20 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__4), 12, 3); -lean_closure_set(x_20, 0, x_3); -lean_closure_set(x_20, 1, x_1); -lean_closure_set(x_20, 2, x_14); -x_21 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1(x_16, x_14, x_20, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); -return x_21; +lean_object* x_16; lean_object* x_17; uint8_t x_18; +x_16 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltRHS(x_2); +x_17 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltDArrow(x_2); +lean_inc(x_16); +x_18 = l_Lean_Elab_Tactic_isHoleRHS(x_16); +if (x_18 == 0) +{ +lean_object* x_19; lean_object* x_20; +lean_inc(x_16); +lean_inc(x_17); +x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__2___boxed), 14, 5); +lean_closure_set(x_19, 0, x_1); +lean_closure_set(x_19, 1, x_2); +lean_closure_set(x_19, 2, x_17); +lean_closure_set(x_19, 3, x_3); +lean_closure_set(x_19, 4, x_16); +x_20 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1(x_17, x_16, x_19, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); +return x_20; +} +else +{ +lean_object* x_21; lean_object* x_22; +lean_inc(x_16); +x_21 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__4___boxed), 13, 4); +lean_closure_set(x_21, 0, x_3); +lean_closure_set(x_21, 1, x_1); +lean_closure_set(x_21, 2, x_2); +lean_closure_set(x_21, 3, x_16); +x_22 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1(x_17, x_16, x_21, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); +return x_22; +} } } } @@ -2086,6 +2321,15 @@ lean_dec(x_2); return x_15; } } +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt___lambda__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, 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) { +_start: +{ +lean_object* x_14; +x_14 = l_Lean_Elab_Tactic_evalAlt___lambda__4(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13); +lean_dec(x_3); +return x_14; +} +} static lean_object* _init_l_Lean_Elab_Tactic_ElimApp_instInhabitedAlt___closed__1() { _start: { @@ -12616,7 +12860,7 @@ lean_closure_set(x_21, 3, x_4); lean_closure_set(x_21, 4, x_5); lean_closure_set(x_21, 5, x_6); x_22 = lean_box(2); -x_23 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_23 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_24 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_24, 0, x_22); lean_ctor_set(x_24, 1, x_23); @@ -17460,7 +17704,7 @@ x_34 = lean_ctor_get(x_15, 11); lean_inc(x_34); x_35 = lean_box(0); x_36 = lean_box(2); -x_37 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_37 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; lean_inc(x_23); x_38 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_38, 0, x_36); @@ -17720,7 +17964,7 @@ x_105 = lean_ctor_get(x_15, 11); lean_inc(x_105); x_106 = lean_box(0); x_107 = lean_box(2); -x_108 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_108 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; lean_inc(x_23); x_109 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_109, 0, x_107); @@ -18312,7 +18556,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__5; x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__6; -x_3 = lean_unsigned_to_nat(469u); +x_3 = lean_unsigned_to_nat(488u); x_4 = lean_unsigned_to_nat(6u); x_5 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__7; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -20555,7 +20799,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = lean_box(2); -x_2 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_3 = l_Lean_Elab_Tactic_ElimApp_mkElimApp___closed__1; x_4 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_4, 0, x_1); @@ -20595,7 +20839,7 @@ x_10 = l_Array_toSubarray___rarg(x_9, x_3, x_5); x_11 = l_Array_ofSubarray___rarg(x_10); lean_dec(x_10); x_12 = lean_box(2); -x_13 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_13 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_14 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_14, 0, x_12); lean_ctor_set(x_14, 1, x_13); @@ -20647,7 +20891,7 @@ x_13 = l_Lean_Syntax_isNone(x_1); if (x_13 == 0) { lean_object* x_14; uint8_t x_15; -x_14 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_14 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; lean_inc(x_3); x_15 = l_Lean_Syntax_isOfKind(x_3, x_14); if (x_15 == 0) @@ -20740,7 +20984,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = lean_box(2); -x_2 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_3 = l_Array_zipWithAux___at_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___spec__2___lambda__1___closed__1; x_4 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_4, 0, x_1); @@ -20781,7 +21025,7 @@ lean_dec(x_1); return x_2; } } -LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(lean_object* x_1) { +LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_shouldExpandAlt(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; @@ -20795,17 +21039,17 @@ lean_dec(x_4); return x_6; } } -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt___boxed(lean_object* x_1) { +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_shouldExpandAlt___boxed(lean_object* x_1) { _start: { uint8_t x_2; lean_object* x_3; -x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(x_1); +x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_shouldExpandAlt(x_1); lean_dec(x_1); x_3 = lean_box(x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) { +LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandAlt_x3f___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) { _start: { uint8_t x_5; @@ -20827,7 +21071,7 @@ lean_ctor_set(x_10, 0, x_6); lean_ctor_set(x_10, 1, x_9); x_11 = lean_array_mk(x_10); x_12 = lean_box(2); -x_13 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_13 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_14 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_14, 0, x_12); lean_ctor_set(x_14, 1, x_13); @@ -20843,11 +21087,11 @@ goto _start; } } } -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f(lean_object* x_1) { +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandAlt_x3f(lean_object* x_1) { _start: { uint8_t x_2; -x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(x_1); +x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_shouldExpandAlt(x_1); if (x_2 == 0) { lean_object* x_3; @@ -20864,14 +21108,14 @@ x_6 = l_Lean_Syntax_getArgs(x_5); lean_dec(x_5); x_7 = lean_array_size(x_6); x_8 = 0; -x_9 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1(x_1, x_7, x_8, x_6); +x_9 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandAlt_x3f___spec__1(x_1, x_7, x_8, x_6); x_10 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_10, 0, x_9); return x_10; } } } -LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandAlt_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { size_t x_5; size_t x_6; lean_object* x_7; @@ -20879,7 +21123,7 @@ x_5 = lean_unbox_usize(x_2); lean_dec(x_2); x_6 = lean_unbox_usize(x_3); lean_dec(x_3); -x_7 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1(x_1, x_5, x_6, x_4); +x_7 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandAlt_x3f___spec__1(x_1, x_5, x_6, x_4); return x_7; } } @@ -20892,7 +21136,7 @@ if (x_4 == 0) { lean_object* x_5; uint8_t x_6; x_5 = lean_array_uget(x_1, x_2); -x_6 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(x_5); +x_6 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_shouldExpandAlt(x_5); lean_dec(x_5); if (x_6 == 0) { @@ -20931,7 +21175,7 @@ else lean_object* x_8; lean_object* x_9; x_8 = lean_array_uget(x_3, x_5); lean_inc(x_8); -x_9 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f(x_8); +x_9 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandAlt_x3f(x_8); if (lean_obj_tag(x_9) == 0) { lean_object* x_10; size_t x_11; size_t x_12; @@ -21001,7 +21245,7 @@ x_13 = l_Lean_Elab_Tactic_ElimApp_mkElimApp___closed__1; x_14 = l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__2(x_2, x_11, x_2, x_12, x_7, x_13); lean_dec(x_2); x_15 = lean_box(2); -x_16 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_16 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_17 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_17, 0, x_15); lean_ctor_set(x_17, 1, x_16); @@ -21106,7 +21350,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__5; x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_inductionAltsPos___closed__5; -x_3 = lean_unsigned_to_nat(577u); +x_3 = lean_unsigned_to_nat(610u); x_4 = lean_unsigned_to_nat(4u); x_5 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_inductionAltsPos___closed__6; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -21212,7 +21456,7 @@ lean_ctor_set(x_12, 0, x_10); lean_ctor_set(x_12, 1, x_11); x_13 = lean_array_mk(x_12); x_14 = lean_box(2); -x_15 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_15 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_16 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_16, 0, x_14); lean_ctor_set(x_16, 1, x_15); @@ -21234,7 +21478,7 @@ lean_ctor_set(x_20, 0, x_18); lean_ctor_set(x_20, 1, x_19); x_21 = lean_array_mk(x_20); x_22 = lean_box(2); -x_23 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_23 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_24 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_24, 0, x_22); lean_ctor_set(x_24, 1, x_23); @@ -25294,7 +25538,7 @@ lean_dec(x_2); return x_10; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__1() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__1() { _start: { lean_object* x_1; @@ -25302,7 +25546,7 @@ x_1 = lean_mk_string_unchecked("tactic", 6, 6); return x_1; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__2() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__2() { _start: { lean_object* x_1; @@ -25310,17 +25554,17 @@ x_1 = lean_mk_string_unchecked("customEliminators", 17, 17); return x_1; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__3() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__1; -x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__2; +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__1; +x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__2; x_3 = l_Lean_Name_mkStr2(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__4() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__4() { _start: { lean_object* x_1; @@ -25328,13 +25572,13 @@ x_1 = lean_mk_string_unchecked("enable using custom eliminators in the 'inductio return x_1; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__5() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__5() { _start: { uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = 1; -x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__1; -x_3 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__4; +x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__1; +x_3 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__4; x_4 = lean_box(x_1); x_5 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_5, 0, x_4); @@ -25343,26 +25587,26 @@ lean_ctor_set(x_5, 2, x_3); return x_5; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__6() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__1; x_2 = l_Lean_Elab_Term_withoutTacticIncrementality___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac___spec__1___closed__2; x_3 = l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___closed__1; -x_4 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__1; -x_5 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__2; +x_4 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__1; +x_5 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__2; x_6 = l_Lean_Name_mkStr5(x_1, x_2, x_3, x_4, x_5); return x_6; } } -LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__3; -x_3 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__5; -x_4 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__6; +x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__3; +x_3 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__5; +x_4 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__6; x_5 = l_Lean_Option_register___at_Lean_Elab_initFn____x40_Lean_Elab_AutoBound___hyg_6____spec__1(x_2, x_3, x_4, x_1); return x_5; } @@ -27429,7 +27673,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__5; x_2 = l_Lean_Elab_Tactic_elabElimTargets___lambda__1___closed__5; -x_3 = lean_unsigned_to_nat(758u); +x_3 = lean_unsigned_to_nat(791u); x_4 = lean_unsigned_to_nat(8u); x_5 = l_Lean_Elab_Tactic_elabElimTargets___lambda__1___closed__4; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -28785,7 +29029,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__5; x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___lambda__1___closed__3; -x_3 = lean_unsigned_to_nat(772u); +x_3 = lean_unsigned_to_nat(805u); x_4 = lean_unsigned_to_nat(6u); x_5 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___lambda__1___closed__2; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -31328,7 +31572,7 @@ x_5 = l_Array_toSubarray___rarg(x_3, x_4, x_1); x_6 = l_Array_ofSubarray___rarg(x_5); lean_dec(x_5); x_7 = lean_box(2); -x_8 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2; +x_8 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2; x_9 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_9, 0, x_7); lean_ctor_set(x_9, 1, x_8); @@ -38110,7 +38354,7 @@ x_3 = l_Lean_Elab_addBuiltinIncrementalElab(x_2, x_1); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__1() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -38120,27 +38364,27 @@ x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__2() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__1; +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__1; x_2 = l_Lean_Elab_Term_withoutTacticIncrementality___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac___spec__1___closed__2; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__3() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__2; +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__2; x_2 = l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___closed__1; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__4() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__4() { _start: { lean_object* x_1; @@ -38148,17 +38392,17 @@ x_1 = lean_mk_string_unchecked("initFn", 6, 6); return x_1; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__5() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__3; -x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__4; +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__3; +x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__4; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__6() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__6() { _start: { lean_object* x_1; @@ -38166,47 +38410,47 @@ x_1 = lean_mk_string_unchecked("_@", 2, 2); return x_1; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__7() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__5; -x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__6; +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__5; +x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__6; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__8() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__7; +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__7; x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__1; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__9() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__9() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__8; +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__8; x_2 = l_Lean_Elab_Term_withoutTacticIncrementality___at_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac___spec__1___closed__2; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__10() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__10() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__9; +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__9; x_2 = l_Lean_Elab_Tactic_ElimApp_evalAlts_goWithInfo___closed__1; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__11() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__11() { _start: { lean_object* x_1; @@ -38214,17 +38458,17 @@ x_1 = lean_mk_string_unchecked("Induction", 9, 9); return x_1; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__12() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__12() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__10; -x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__11; +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__10; +x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__11; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__13() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__13() { _start: { lean_object* x_1; @@ -38232,33 +38476,33 @@ x_1 = lean_mk_string_unchecked("_hyg", 4, 4); return x_1; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__14() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__14() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__12; -x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__13; +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__12; +x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__13; x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__15() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__15() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__14; -x_2 = lean_unsigned_to_nat(14427u); +x_1 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__14; +x_2 = lean_unsigned_to_nat(14993u); x_3 = l_Lean_Name_num___override(x_1, x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993_(lean_object* x_1) { _start: { lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Expr_withAppAux___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabFunTarget___spec__5___lambda__3___closed__8; x_3 = 0; -x_4 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__15; +x_4 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__15; x_5 = l_Lean_registerTraceClass(x_2, x_3, x_4, x_1); if (lean_obj_tag(x_5) == 0) { @@ -38369,18 +38613,22 @@ l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__ lean_mark_persistent(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__6); l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__7 = _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__7(); lean_mark_persistent(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__7); +l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__1 = _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__1(); +lean_mark_persistent(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__1); +l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2 = _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2(); +lean_mark_persistent(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_hasAltRHS___closed__2); l_Lean_Elab_Tactic_isHoleRHS___closed__1 = _init_l_Lean_Elab_Tactic_isHoleRHS___closed__1(); lean_mark_persistent(l_Lean_Elab_Tactic_isHoleRHS___closed__1); l_Lean_Elab_Tactic_isHoleRHS___closed__2 = _init_l_Lean_Elab_Tactic_isHoleRHS___closed__2(); lean_mark_persistent(l_Lean_Elab_Tactic_isHoleRHS___closed__2); -l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__1 = _init_l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__1(); -lean_mark_persistent(l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__1); -l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2 = _init_l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2(); -lean_mark_persistent(l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1___closed__2); l_Lean_Elab_Tactic_evalAlt___lambda__3___closed__1 = _init_l_Lean_Elab_Tactic_evalAlt___lambda__3___closed__1(); lean_mark_persistent(l_Lean_Elab_Tactic_evalAlt___lambda__3___closed__1); l_Lean_Elab_Tactic_evalAlt___lambda__3___closed__2 = _init_l_Lean_Elab_Tactic_evalAlt___lambda__3___closed__2(); lean_mark_persistent(l_Lean_Elab_Tactic_evalAlt___lambda__3___closed__2); +l_Lean_Elab_Tactic_evalAlt___closed__1 = _init_l_Lean_Elab_Tactic_evalAlt___closed__1(); +lean_mark_persistent(l_Lean_Elab_Tactic_evalAlt___closed__1); +l_Lean_Elab_Tactic_evalAlt___closed__2 = _init_l_Lean_Elab_Tactic_evalAlt___closed__2(); +lean_mark_persistent(l_Lean_Elab_Tactic_evalAlt___closed__2); l_Lean_Elab_Tactic_ElimApp_instInhabitedAlt___closed__1 = _init_l_Lean_Elab_Tactic_ElimApp_instInhabitedAlt___closed__1(); lean_mark_persistent(l_Lean_Elab_Tactic_ElimApp_instInhabitedAlt___closed__1); l_Lean_Elab_Tactic_ElimApp_instInhabitedAlt___closed__2 = _init_l_Lean_Elab_Tactic_ElimApp_instInhabitedAlt___closed__2(); @@ -38633,19 +38881,19 @@ l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__2___closed__13 = _init_l_L lean_mark_persistent(l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__2___closed__13); l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabTermForElim___closed__1 = _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabTermForElim___closed__1(); lean_mark_persistent(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabTermForElim___closed__1); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__1(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__1); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__2 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__2(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__2); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__3 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__3(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__3); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__4 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__4(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__4); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__5 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__5(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__5); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__6 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__6(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890____closed__6); -if (builtin) {res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_8890_(lean_io_mk_world()); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__1(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__1); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__2 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__2(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__2); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__3 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__3(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__3); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__4 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__4(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__4); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__5 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__5(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__5); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__6 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__6(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456____closed__6); +if (builtin) {res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_9456_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Elab_Tactic_tactic_customEliminators = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Elab_Tactic_tactic_customEliminators); @@ -38922,37 +39170,37 @@ lean_dec_ref(res); }if (builtin) {res = l___regBuiltin_Lean_Elab_Tactic_evalFunCases__2(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -}l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__1(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__1); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__2 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__2(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__2); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__3 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__3(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__3); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__4 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__4(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__4); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__5 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__5(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__5); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__6 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__6(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__6); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__7 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__7(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__7); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__8 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__8(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__8); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__9 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__9(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__9); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__10 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__10(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__10); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__11 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__11(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__11); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__12 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__12(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__12); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__13 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__13(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__13); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__14 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__14(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__14); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__15 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__15(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427____closed__15); -if (builtin) {res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14427_(lean_io_mk_world()); +}l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__1(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__1); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__2 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__2(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__2); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__3 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__3(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__3); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__4 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__4(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__4); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__5 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__5(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__5); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__6 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__6(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__6); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__7 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__7(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__7); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__8 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__8(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__8); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__9 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__9(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__9); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__10 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__10(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__10); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__11 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__11(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__11); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__12 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__12(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__12); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__13 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__13(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__13); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__14 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__14(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__14); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__15 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__15(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993____closed__15); +if (builtin) {res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_14993_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); }return lean_io_result_mk_ok(lean_box(0)); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Grind/ExtAttr.c b/stage0/stdlib/Lean/Meta/Tactic/Grind/ExtAttr.c index 5d476af5b8..37c974f12f 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Grind/ExtAttr.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/ExtAttr.c @@ -190,7 +190,7 @@ static lean_object* _init_l_Lean_Meta_Grind_validateExtAttr___closed__3() { _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("` is tagged with `[ext]`", 24, 24); +x_1 = lean_mk_string_unchecked("` is not tagged with `[ext]`", 28, 28); return x_1; } }