From 2dad133208b07337cff9484e1bc3b6ee34ecafc7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Jun 2022 11:26:06 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Tactics.lean | 3 +- stage0/src/Lean/Elab/Tactic/Induction.lean | 32 +- stage0/stdlib/Init/Classical.c | 1576 +++++++++++--------- stage0/stdlib/Init/Tactics.c | 417 +++--- stage0/stdlib/Lean/Elab/Tactic/Induction.c | 208 +-- 5 files changed, 1159 insertions(+), 1077 deletions(-) diff --git a/stage0/src/Init/Tactics.lean b/stage0/src/Init/Tactics.lean index 703e8e2102..46ad7afbcf 100644 --- a/stage0/src/Init/Tactics.lean +++ b/stage0/src/Init/Tactics.lean @@ -316,7 +316,8 @@ macro "have' " d:haveDecl : tactic => `(refine_lift' have $d:haveDecl; ?_) macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x:ident : _ := $p) macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_) -syntax inductionAlt := ppDedent(ppLine) "| " (group("@"? ident) <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq) +syntax inductionAltLHS := "| " (group("@"? ident) <|> "_") (ident <|> "_")* +syntax inductionAlt := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq) syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+) /-- Assuming `x` is a variable in the local context with an inductive type, `induction x` applies induction on `x` to the main goal, diff --git a/stage0/src/Lean/Elab/Tactic/Induction.lean b/stage0/src/Lean/Elab/Tactic/Induction.lean index abad5df0db..f5085df926 100644 --- a/stage0/src/Lean/Elab/Tactic/Induction.lean +++ b/stage0/src/Lean/Elab/Tactic/Induction.lean @@ -21,18 +21,12 @@ open Meta /- Given an `inductionAlt` of the form ``` - syntax inductionAlt := ppDedent(ppLine) "| " (group("@"? ident) <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq) - ``` - going to change to - ``` - syntax inductionAlt := ppDedent(ppLine) ("| " (group("@"? ident) <|> "_") (ident <|> "_")*)+ " => " (hole <|> syntheticHole <|> tacticSeq) + syntax inductionAltLHS := "| " (group("@"? ident) <|> "_") (ident <|> "_")* + syntax inductionAlt := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq) ``` -/ -private def isNewAlt (alt : Syntax) : Bool := - alt.getNumArgs == 3 - private def isMultiAlt (alt : Syntax) : Bool := - isNewAlt alt && alt[0].getNumArgs > 1 + alt[0].getNumArgs > 1 private def expandMultiAlt? (alt : Syntax) : Option (Array Syntax) := Id.run do if isMultiAlt alt then @@ -41,33 +35,27 @@ private def expandMultiAlt? (alt : Syntax) : Option (Array Syntax) := Id.run do none private def getFirstAltLhs (alt : Syntax) : Syntax := - if isNewAlt alt then -- TODO: delete - alt[0][0] - else -- TODO: delete - alt -- TODO: delete + alt[0][0] -/-- Return `inductionAlt` name. It assumes `alt` is not a multi alternative. -/ +/-- Return `inductionAlt` name. It assumes `alt` does not have multiple `inductionAltLHS` -/ private def getAltName (alt : Syntax) : Name := let lhs := getFirstAltLhs alt if lhs[1].hasArgs then lhs[1][1].getId.eraseMacroScopes else `_ +/-- Return `true` if the first LHS of the given alternative contains `@`. -/ private def altHasExplicitModifier (alt : Syntax) : Bool := let lhs := getFirstAltLhs alt lhs[1].hasArgs && !lhs[1][0].isNone +/-- Return the variables in the first LHS of the given alternative. -/ private def getAltVars (alt : Syntax) : Array Syntax := let lhs := getFirstAltLhs alt lhs[2].getArgs +/-- Return the variable names in the first LHS of the given alternative. -/ private def getAltVarNames (alt : Syntax) : Array Name := getAltVars alt |>.map getNameOfIdent' private def getAltRHS (alt : Syntax) : Syntax := - if isNewAlt alt then -- TODO: delete - alt[2] - else -- TODO: delete - alt[4] -- TODO: delete + alt[2] private def getAltDArrow (alt : Syntax) : Syntax := - if isNewAlt alt then -- TODO: delete - alt[1] - else -- TODO: delete - alt[3] -- TODO: delete + alt[1] -- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic def isHoleRHS (rhs : Syntax) : Bool := diff --git a/stage0/stdlib/Init/Classical.c b/stage0/stdlib/Init/Classical.c index e70e5b704b..f976b83bf6 100644 --- a/stage0/stdlib/Init/Classical.c +++ b/stage0/stdlib/Init/Classical.c @@ -100,6 +100,7 @@ static lean_object* l_Classical___aux__Init__Classical______macroRules__Classica static lean_object* l_Classical_tacticBy__cases_____x3a_____closed__19; static lean_object* l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__14; static lean_object* l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__15; +static lean_object* l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__56; static lean_object* l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__18; static lean_object* l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__30; static lean_object* l_Classical_tacticBy__cases_____x3a_____closed__21; @@ -698,62 +699,39 @@ static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Cl _start: { lean_object* x_1; -x_1 = lean_mk_string_from_bytes("|", 1); +x_1 = lean_mk_string_from_bytes("inductionAltLHS", 15); return x_1; } } static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__35() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__6; +x_2 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__34; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__36() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("|", 1); +return x_1; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__37() { +_start: +{ lean_object* x_1; x_1 = lean_mk_string_from_bytes("group", 5); return x_1; } } -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__36() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__35; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__37() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string_from_bytes("inl", 3); -return x_1; -} -} static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__38() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__37; -x_2 = lean_string_utf8_byte_size(x_1); -return x_2; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__39() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__37; -x_2 = lean_unsigned_to_nat(0u); -x_3 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__38; -x_4 = lean_alloc_ctor(0, 3, 0); -lean_ctor_set(x_4, 0, x_1); -lean_ctor_set(x_4, 1, x_2); -lean_ctor_set(x_4, 2, x_3); -return x_4; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__40() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); x_2 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__37; @@ -761,114 +739,71 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__39() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("inl", 3); +return x_1; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__40() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__39; +x_2 = lean_string_utf8_byte_size(x_1); +return x_2; +} +} static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__41() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__39; +x_2 = lean_unsigned_to_nat(0u); +x_3 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__40; +x_4 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__42() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__39; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__43() { +_start: +{ lean_object* x_1; x_1 = lean_mk_string_from_bytes("h", 1); return x_1; } } -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__42() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__41; -x_2 = lean_string_utf8_byte_size(x_1); -return x_2; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__43() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__41; -x_2 = lean_unsigned_to_nat(0u); -x_3 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__42; -x_4 = lean_alloc_ctor(0, 3, 0); -lean_ctor_set(x_4, 0, x_1); -lean_ctor_set(x_4, 1, x_2); -lean_ctor_set(x_4, 2, x_3); -return x_4; -} -} static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__44() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__41; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; +lean_object* x_1; lean_object* x_2; +x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__43; +x_2 = lean_string_utf8_byte_size(x_1); +return x_2; } } static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__45() { _start: { -lean_object* x_1; -x_1 = lean_mk_string_from_bytes("=>", 2); -return x_1; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__46() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string_from_bytes("hole", 4); -return x_1; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__47() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__16; -x_2 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__46; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__48() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string_from_bytes("_", 1); -return x_1; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__49() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = lean_unsigned_to_nat(5u); -x_2 = lean_mk_empty_array_with_capacity(x_1); -return x_2; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__50() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string_from_bytes("inr", 3); -return x_1; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__51() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__50; -x_2 = lean_string_utf8_byte_size(x_1); -return x_2; -} -} -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__52() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__50; +x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__43; x_2 = lean_unsigned_to_nat(0u); -x_3 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__51; +x_3 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__44; x_4 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -876,17 +811,17 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__53() { +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__46() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__50; +x_2 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__43; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54() { +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__47() { _start: { lean_object* x_1; lean_object* x_2; @@ -895,9 +830,84 @@ x_2 = lean_mk_empty_array_with_capacity(x_1); return x_2; } } +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__48() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("=>", 2); +return x_1; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__49() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("hole", 4); +return x_1; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__50() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__16; +x_2 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__49; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__51() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("_", 1); +return x_1; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__52() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("inr", 3); +return x_1; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__53() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__52; +x_2 = lean_string_utf8_byte_size(x_1); +return x_2; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__52; +x_2 = lean_unsigned_to_nat(0u); +x_3 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__53; +x_4 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__52; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__56() { +_start: +{ lean_object* x_1; lean_object* x_2; x_1 = lean_unsigned_to_nat(4u); x_2 = lean_mk_empty_array_with_capacity(x_1); @@ -957,7 +967,7 @@ x_18 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRul x_19 = !lean_is_exclusive(x_18); if (x_19 == 0) { -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; 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; 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; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; 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; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; +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; 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; 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; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; 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; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; 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; lean_object* x_116; x_20 = lean_ctor_get(x_18, 0); x_21 = lean_ctor_get(x_2, 2); lean_inc(x_21); @@ -1015,16 +1025,16 @@ lean_inc(x_20); x_48 = lean_alloc_ctor(2, 2, 0); lean_ctor_set(x_48, 0, x_20); lean_ctor_set(x_48, 1, x_47); -x_49 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__34; +x_49 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__36; lean_inc(x_20); x_50 = lean_alloc_ctor(2, 2, 0); lean_ctor_set(x_50, 0, x_20); lean_ctor_set(x_50, 1, x_49); -x_51 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__40; +x_51 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__42; lean_inc(x_21); lean_inc(x_22); x_52 = l_Lean_addMacroScope(x_22, x_51, x_21); -x_53 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__39; +x_53 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__41; lean_inc(x_20); x_54 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_54, 0, x_20); @@ -1032,16 +1042,16 @@ lean_ctor_set(x_54, 1, x_53); lean_ctor_set(x_54, 2, x_52); lean_ctor_set(x_54, 3, x_27); x_55 = lean_array_push(x_41, x_54); -x_56 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__36; +x_56 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__38; x_57 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_57, 0, x_33); lean_ctor_set(x_57, 1, x_56); lean_ctor_set(x_57, 2, x_55); -x_58 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__44; +x_58 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__46; lean_inc(x_21); lean_inc(x_22); x_59 = l_Lean_addMacroScope(x_22, x_58, x_21); -x_60 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__43; +x_60 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__45; lean_inc(x_20); x_61 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_61, 0, x_20); @@ -1053,664 +1063,744 @@ x_63 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_63, 0, x_33); lean_ctor_set(x_63, 1, x_34); lean_ctor_set(x_63, 2, x_62); -x_64 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__45; -lean_inc(x_20); -x_65 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_65, 0, x_20); -lean_ctor_set(x_65, 1, x_64); -x_66 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__48; -lean_inc(x_20); -x_67 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_67, 0, x_20); -lean_ctor_set(x_67, 1, x_66); -x_68 = lean_array_push(x_31, x_67); -x_69 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__47; -x_70 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_70, 0, x_33); -lean_ctor_set(x_70, 1, x_69); -lean_ctor_set(x_70, 2, x_68); -x_71 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__49; -x_72 = lean_array_push(x_71, x_50); -lean_inc(x_72); -x_73 = lean_array_push(x_72, x_57); -lean_inc(x_63); -x_74 = lean_array_push(x_73, x_63); +x_64 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__47; +x_65 = lean_array_push(x_64, x_50); lean_inc(x_65); -x_75 = lean_array_push(x_74, x_65); -lean_inc(x_70); -x_76 = lean_array_push(x_75, x_70); -x_77 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__33; +x_66 = lean_array_push(x_65, x_57); +lean_inc(x_63); +x_67 = lean_array_push(x_66, x_63); +x_68 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__35; +x_69 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_69, 0, x_33); +lean_ctor_set(x_69, 1, x_68); +lean_ctor_set(x_69, 2, x_67); +x_70 = lean_array_push(x_31, x_69); +x_71 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_71, 0, x_33); +lean_ctor_set(x_71, 1, x_34); +lean_ctor_set(x_71, 2, x_70); +x_72 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__48; +lean_inc(x_20); +x_73 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_73, 0, x_20); +lean_ctor_set(x_73, 1, x_72); +x_74 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__51; +lean_inc(x_20); +x_75 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_75, 0, x_20); +lean_ctor_set(x_75, 1, x_74); +x_76 = lean_array_push(x_31, x_75); +x_77 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__50; x_78 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_78, 0, x_33); lean_ctor_set(x_78, 1, x_77); lean_ctor_set(x_78, 2, x_76); -x_79 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__53; -x_80 = l_Lean_addMacroScope(x_22, x_79, x_21); -x_81 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__52; -x_82 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_82, 0, x_20); -lean_ctor_set(x_82, 1, x_81); -lean_ctor_set(x_82, 2, x_80); -lean_ctor_set(x_82, 3, x_27); -x_83 = lean_array_push(x_41, x_82); -x_84 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_84, 0, x_33); -lean_ctor_set(x_84, 1, x_56); -lean_ctor_set(x_84, 2, x_83); -x_85 = lean_array_push(x_72, x_84); -x_86 = lean_array_push(x_85, x_63); -x_87 = lean_array_push(x_86, x_65); -x_88 = lean_array_push(x_87, x_70); +x_79 = lean_array_push(x_64, x_71); +lean_inc(x_73); +x_80 = lean_array_push(x_79, x_73); +lean_inc(x_78); +x_81 = lean_array_push(x_80, x_78); +x_82 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__33; +x_83 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_83, 0, x_33); +lean_ctor_set(x_83, 1, x_82); +lean_ctor_set(x_83, 2, x_81); +x_84 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55; +x_85 = l_Lean_addMacroScope(x_22, x_84, x_21); +x_86 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54; +x_87 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_87, 0, x_20); +lean_ctor_set(x_87, 1, x_86); +lean_ctor_set(x_87, 2, x_85); +lean_ctor_set(x_87, 3, x_27); +x_88 = lean_array_push(x_41, x_87); x_89 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_89, 0, x_33); -lean_ctor_set(x_89, 1, x_77); +lean_ctor_set(x_89, 1, x_56); lean_ctor_set(x_89, 2, x_88); -x_90 = lean_array_push(x_36, x_78); -x_91 = lean_array_push(x_90, x_89); +x_90 = lean_array_push(x_65, x_89); +x_91 = lean_array_push(x_90, x_63); x_92 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_92, 0, x_33); -lean_ctor_set(x_92, 1, x_34); +lean_ctor_set(x_92, 1, x_68); lean_ctor_set(x_92, 2, x_91); -x_93 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54; -x_94 = lean_array_push(x_93, x_48); -x_95 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__14; -x_96 = lean_array_push(x_94, x_95); -x_97 = lean_array_push(x_96, x_92); -x_98 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__30; -x_99 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_99, 0, x_33); -lean_ctor_set(x_99, 1, x_98); -lean_ctor_set(x_99, 2, x_97); -x_100 = lean_array_push(x_31, x_99); +x_93 = lean_array_push(x_31, x_92); +x_94 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_94, 0, x_33); +lean_ctor_set(x_94, 1, x_34); +lean_ctor_set(x_94, 2, x_93); +x_95 = lean_array_push(x_64, x_94); +x_96 = lean_array_push(x_95, x_73); +x_97 = lean_array_push(x_96, x_78); +x_98 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_98, 0, x_33); +lean_ctor_set(x_98, 1, x_82); +lean_ctor_set(x_98, 2, x_97); +x_99 = lean_array_push(x_36, x_83); +x_100 = lean_array_push(x_99, x_98); x_101 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_101, 0, x_33); lean_ctor_set(x_101, 1, x_34); lean_ctor_set(x_101, 2, x_100); -x_102 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55; -x_103 = lean_array_push(x_102, x_24); -x_104 = lean_array_push(x_103, x_46); -x_105 = lean_array_push(x_104, x_95); -x_106 = lean_array_push(x_105, x_101); -x_107 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__8; -x_108 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_108, 0, x_33); -lean_ctor_set(x_108, 1, x_107); -lean_ctor_set(x_108, 2, x_106); -lean_ctor_set(x_18, 0, x_108); +x_102 = lean_array_push(x_64, x_48); +x_103 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__14; +x_104 = lean_array_push(x_102, x_103); +x_105 = lean_array_push(x_104, x_101); +x_106 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__30; +x_107 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_107, 0, x_33); +lean_ctor_set(x_107, 1, x_106); +lean_ctor_set(x_107, 2, x_105); +x_108 = lean_array_push(x_31, x_107); +x_109 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_109, 0, x_33); +lean_ctor_set(x_109, 1, x_34); +lean_ctor_set(x_109, 2, x_108); +x_110 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__56; +x_111 = lean_array_push(x_110, x_24); +x_112 = lean_array_push(x_111, x_46); +x_113 = lean_array_push(x_112, x_103); +x_114 = lean_array_push(x_113, x_109); +x_115 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__8; +x_116 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_116, 0, x_33); +lean_ctor_set(x_116, 1, x_115); +lean_ctor_set(x_116, 2, x_114); +lean_ctor_set(x_18, 0, x_116); return x_18; } else { -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; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; 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; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; 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; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; lean_object* x_192; lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; -x_109 = lean_ctor_get(x_18, 0); -x_110 = lean_ctor_get(x_18, 1); -lean_inc(x_110); -lean_inc(x_109); +lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; 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; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; 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; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172; lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178; lean_object* x_179; lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; lean_object* x_192; lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200; lean_object* x_201; lean_object* x_202; lean_object* x_203; lean_object* x_204; lean_object* x_205; lean_object* x_206; lean_object* x_207; lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; +x_117 = lean_ctor_get(x_18, 0); +x_118 = lean_ctor_get(x_18, 1); +lean_inc(x_118); +lean_inc(x_117); lean_dec(x_18); -x_111 = lean_ctor_get(x_2, 2); -lean_inc(x_111); -x_112 = lean_ctor_get(x_2, 1); -lean_inc(x_112); +x_119 = lean_ctor_get(x_2, 2); +lean_inc(x_119); +x_120 = lean_ctor_get(x_2, 1); +lean_inc(x_120); lean_dec(x_2); -x_113 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__7; -lean_inc(x_109); -x_114 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_114, 0, x_109); -lean_ctor_set(x_114, 1, x_113); -x_115 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__22; -lean_inc(x_111); -lean_inc(x_112); -x_116 = l_Lean_addMacroScope(x_112, x_115, x_111); -x_117 = lean_box(0); -x_118 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__21; -x_119 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__25; -lean_inc(x_109); -x_120 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_120, 0, x_109); -lean_ctor_set(x_120, 1, x_118); -lean_ctor_set(x_120, 2, x_116); -lean_ctor_set(x_120, 3, x_119); -x_121 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__26; -x_122 = lean_array_push(x_121, x_17); -x_123 = lean_box(2); -x_124 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__10; -x_125 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_125, 0, x_123); -lean_ctor_set(x_125, 1, x_124); -lean_ctor_set(x_125, 2, x_122); -x_126 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__27; -x_127 = lean_array_push(x_126, x_120); -x_128 = lean_array_push(x_127, x_125); -x_129 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__18; -x_130 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_130, 0, x_123); -lean_ctor_set(x_130, 1, x_129); -lean_ctor_set(x_130, 2, x_128); -x_131 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__28; -x_132 = lean_array_push(x_131, x_130); -x_133 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__12; -x_134 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_134, 0, x_123); -lean_ctor_set(x_134, 1, x_133); -lean_ctor_set(x_134, 2, x_132); -x_135 = lean_array_push(x_121, x_134); -x_136 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_136, 0, x_123); -lean_ctor_set(x_136, 1, x_124); -lean_ctor_set(x_136, 2, x_135); -x_137 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__31; -lean_inc(x_109); -x_138 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_138, 0, x_109); +x_121 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__7; +lean_inc(x_117); +x_122 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_122, 0, x_117); +lean_ctor_set(x_122, 1, x_121); +x_123 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__22; +lean_inc(x_119); +lean_inc(x_120); +x_124 = l_Lean_addMacroScope(x_120, x_123, x_119); +x_125 = lean_box(0); +x_126 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__21; +x_127 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__25; +lean_inc(x_117); +x_128 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_128, 0, x_117); +lean_ctor_set(x_128, 1, x_126); +lean_ctor_set(x_128, 2, x_124); +lean_ctor_set(x_128, 3, x_127); +x_129 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__26; +x_130 = lean_array_push(x_129, x_17); +x_131 = lean_box(2); +x_132 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__10; +x_133 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_133, 0, x_131); +lean_ctor_set(x_133, 1, x_132); +lean_ctor_set(x_133, 2, x_130); +x_134 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__27; +x_135 = lean_array_push(x_134, x_128); +x_136 = lean_array_push(x_135, x_133); +x_137 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__18; +x_138 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_138, 0, x_131); lean_ctor_set(x_138, 1, x_137); -x_139 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__34; -lean_inc(x_109); -x_140 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_140, 0, x_109); -lean_ctor_set(x_140, 1, x_139); -x_141 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__40; -lean_inc(x_111); -lean_inc(x_112); -x_142 = l_Lean_addMacroScope(x_112, x_141, x_111); -x_143 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__39; -lean_inc(x_109); -x_144 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_144, 0, x_109); -lean_ctor_set(x_144, 1, x_143); -lean_ctor_set(x_144, 2, x_142); -lean_ctor_set(x_144, 3, x_117); -x_145 = lean_array_push(x_131, x_144); -x_146 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__36; -x_147 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_147, 0, x_123); -lean_ctor_set(x_147, 1, x_146); -lean_ctor_set(x_147, 2, x_145); -x_148 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__44; -lean_inc(x_111); -lean_inc(x_112); -x_149 = l_Lean_addMacroScope(x_112, x_148, x_111); -x_150 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__43; -lean_inc(x_109); -x_151 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_151, 0, x_109); -lean_ctor_set(x_151, 1, x_150); -lean_ctor_set(x_151, 2, x_149); -lean_ctor_set(x_151, 3, x_117); -x_152 = lean_array_push(x_121, x_151); -x_153 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_153, 0, x_123); -lean_ctor_set(x_153, 1, x_124); -lean_ctor_set(x_153, 2, x_152); -x_154 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__45; -lean_inc(x_109); -x_155 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_155, 0, x_109); +lean_ctor_set(x_138, 2, x_136); +x_139 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__28; +x_140 = lean_array_push(x_139, x_138); +x_141 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__12; +x_142 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_142, 0, x_131); +lean_ctor_set(x_142, 1, x_141); +lean_ctor_set(x_142, 2, x_140); +x_143 = lean_array_push(x_129, x_142); +x_144 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_144, 0, x_131); +lean_ctor_set(x_144, 1, x_132); +lean_ctor_set(x_144, 2, x_143); +x_145 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__31; +lean_inc(x_117); +x_146 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_146, 0, x_117); +lean_ctor_set(x_146, 1, x_145); +x_147 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__36; +lean_inc(x_117); +x_148 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_148, 0, x_117); +lean_ctor_set(x_148, 1, x_147); +x_149 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__42; +lean_inc(x_119); +lean_inc(x_120); +x_150 = l_Lean_addMacroScope(x_120, x_149, x_119); +x_151 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__41; +lean_inc(x_117); +x_152 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_152, 0, x_117); +lean_ctor_set(x_152, 1, x_151); +lean_ctor_set(x_152, 2, x_150); +lean_ctor_set(x_152, 3, x_125); +x_153 = lean_array_push(x_139, x_152); +x_154 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__38; +x_155 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_155, 0, x_131); lean_ctor_set(x_155, 1, x_154); -x_156 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__48; -lean_inc(x_109); -x_157 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_157, 0, x_109); -lean_ctor_set(x_157, 1, x_156); -x_158 = lean_array_push(x_121, x_157); -x_159 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__47; -x_160 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_160, 0, x_123); -lean_ctor_set(x_160, 1, x_159); -lean_ctor_set(x_160, 2, x_158); -x_161 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__49; -x_162 = lean_array_push(x_161, x_140); -lean_inc(x_162); -x_163 = lean_array_push(x_162, x_147); -lean_inc(x_153); -x_164 = lean_array_push(x_163, x_153); -lean_inc(x_155); -x_165 = lean_array_push(x_164, x_155); -lean_inc(x_160); -x_166 = lean_array_push(x_165, x_160); -x_167 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__33; -x_168 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_168, 0, x_123); -lean_ctor_set(x_168, 1, x_167); -lean_ctor_set(x_168, 2, x_166); -x_169 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__53; -x_170 = l_Lean_addMacroScope(x_112, x_169, x_111); -x_171 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__52; -x_172 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_172, 0, x_109); -lean_ctor_set(x_172, 1, x_171); -lean_ctor_set(x_172, 2, x_170); -lean_ctor_set(x_172, 3, x_117); -x_173 = lean_array_push(x_131, x_172); -x_174 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_174, 0, x_123); -lean_ctor_set(x_174, 1, x_146); -lean_ctor_set(x_174, 2, x_173); -x_175 = lean_array_push(x_162, x_174); -x_176 = lean_array_push(x_175, x_153); -x_177 = lean_array_push(x_176, x_155); -x_178 = lean_array_push(x_177, x_160); -x_179 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_179, 0, x_123); -lean_ctor_set(x_179, 1, x_167); -lean_ctor_set(x_179, 2, x_178); -x_180 = lean_array_push(x_126, x_168); -x_181 = lean_array_push(x_180, x_179); -x_182 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_182, 0, x_123); -lean_ctor_set(x_182, 1, x_124); -lean_ctor_set(x_182, 2, x_181); -x_183 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54; -x_184 = lean_array_push(x_183, x_138); -x_185 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__14; -x_186 = lean_array_push(x_184, x_185); -x_187 = lean_array_push(x_186, x_182); -x_188 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__30; -x_189 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_189, 0, x_123); -lean_ctor_set(x_189, 1, x_188); -lean_ctor_set(x_189, 2, x_187); -x_190 = lean_array_push(x_121, x_189); -x_191 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_191, 0, x_123); -lean_ctor_set(x_191, 1, x_124); -lean_ctor_set(x_191, 2, x_190); -x_192 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55; -x_193 = lean_array_push(x_192, x_114); -x_194 = lean_array_push(x_193, x_136); -x_195 = lean_array_push(x_194, x_185); -x_196 = lean_array_push(x_195, x_191); -x_197 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__8; -x_198 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_198, 0, x_123); -lean_ctor_set(x_198, 1, x_197); -lean_ctor_set(x_198, 2, x_196); -x_199 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_199, 0, x_198); -lean_ctor_set(x_199, 1, x_110); -return x_199; +lean_ctor_set(x_155, 2, x_153); +x_156 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__46; +lean_inc(x_119); +lean_inc(x_120); +x_157 = l_Lean_addMacroScope(x_120, x_156, x_119); +x_158 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__45; +lean_inc(x_117); +x_159 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_159, 0, x_117); +lean_ctor_set(x_159, 1, x_158); +lean_ctor_set(x_159, 2, x_157); +lean_ctor_set(x_159, 3, x_125); +x_160 = lean_array_push(x_129, x_159); +x_161 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_161, 0, x_131); +lean_ctor_set(x_161, 1, x_132); +lean_ctor_set(x_161, 2, x_160); +x_162 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__47; +x_163 = lean_array_push(x_162, x_148); +lean_inc(x_163); +x_164 = lean_array_push(x_163, x_155); +lean_inc(x_161); +x_165 = lean_array_push(x_164, x_161); +x_166 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__35; +x_167 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_167, 0, x_131); +lean_ctor_set(x_167, 1, x_166); +lean_ctor_set(x_167, 2, x_165); +x_168 = lean_array_push(x_129, x_167); +x_169 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_169, 0, x_131); +lean_ctor_set(x_169, 1, x_132); +lean_ctor_set(x_169, 2, x_168); +x_170 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__48; +lean_inc(x_117); +x_171 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_171, 0, x_117); +lean_ctor_set(x_171, 1, x_170); +x_172 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__51; +lean_inc(x_117); +x_173 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_173, 0, x_117); +lean_ctor_set(x_173, 1, x_172); +x_174 = lean_array_push(x_129, x_173); +x_175 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__50; +x_176 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_176, 0, x_131); +lean_ctor_set(x_176, 1, x_175); +lean_ctor_set(x_176, 2, x_174); +x_177 = lean_array_push(x_162, x_169); +lean_inc(x_171); +x_178 = lean_array_push(x_177, x_171); +lean_inc(x_176); +x_179 = lean_array_push(x_178, x_176); +x_180 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__33; +x_181 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_181, 0, x_131); +lean_ctor_set(x_181, 1, x_180); +lean_ctor_set(x_181, 2, x_179); +x_182 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55; +x_183 = l_Lean_addMacroScope(x_120, x_182, x_119); +x_184 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54; +x_185 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_185, 0, x_117); +lean_ctor_set(x_185, 1, x_184); +lean_ctor_set(x_185, 2, x_183); +lean_ctor_set(x_185, 3, x_125); +x_186 = lean_array_push(x_139, x_185); +x_187 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_187, 0, x_131); +lean_ctor_set(x_187, 1, x_154); +lean_ctor_set(x_187, 2, x_186); +x_188 = lean_array_push(x_163, x_187); +x_189 = lean_array_push(x_188, x_161); +x_190 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_190, 0, x_131); +lean_ctor_set(x_190, 1, x_166); +lean_ctor_set(x_190, 2, x_189); +x_191 = lean_array_push(x_129, x_190); +x_192 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_192, 0, x_131); +lean_ctor_set(x_192, 1, x_132); +lean_ctor_set(x_192, 2, x_191); +x_193 = lean_array_push(x_162, x_192); +x_194 = lean_array_push(x_193, x_171); +x_195 = lean_array_push(x_194, x_176); +x_196 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_196, 0, x_131); +lean_ctor_set(x_196, 1, x_180); +lean_ctor_set(x_196, 2, x_195); +x_197 = lean_array_push(x_134, x_181); +x_198 = lean_array_push(x_197, x_196); +x_199 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_199, 0, x_131); +lean_ctor_set(x_199, 1, x_132); +lean_ctor_set(x_199, 2, x_198); +x_200 = lean_array_push(x_162, x_146); +x_201 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__14; +x_202 = lean_array_push(x_200, x_201); +x_203 = lean_array_push(x_202, x_199); +x_204 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__30; +x_205 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_205, 0, x_131); +lean_ctor_set(x_205, 1, x_204); +lean_ctor_set(x_205, 2, x_203); +x_206 = lean_array_push(x_129, x_205); +x_207 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_207, 0, x_131); +lean_ctor_set(x_207, 1, x_132); +lean_ctor_set(x_207, 2, x_206); +x_208 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__56; +x_209 = lean_array_push(x_208, x_122); +x_210 = lean_array_push(x_209, x_144); +x_211 = lean_array_push(x_210, x_201); +x_212 = lean_array_push(x_211, x_207); +x_213 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__8; +x_214 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_214, 0, x_131); +lean_ctor_set(x_214, 1, x_213); +lean_ctor_set(x_214, 2, x_212); +x_215 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_215, 0, x_214); +lean_ctor_set(x_215, 1, x_118); +return x_215; } } } else { -lean_object* x_200; lean_object* x_201; lean_object* x_202; uint8_t x_203; -x_200 = lean_unsigned_to_nat(0u); -x_201 = l_Lean_Syntax_getArg(x_9, x_200); +lean_object* x_216; lean_object* x_217; lean_object* x_218; uint8_t x_219; +x_216 = lean_unsigned_to_nat(0u); +x_217 = l_Lean_Syntax_getArg(x_9, x_216); lean_dec(x_9); -x_202 = l_Classical_tacticBy__cases_____x3a_____closed__14; -lean_inc(x_201); -x_203 = l_Lean_Syntax_isOfKind(x_201, x_202); -if (x_203 == 0) +x_218 = l_Classical_tacticBy__cases_____x3a_____closed__14; +lean_inc(x_217); +x_219 = l_Lean_Syntax_isOfKind(x_217, x_218); +if (x_219 == 0) { -lean_object* x_204; lean_object* x_205; -lean_dec(x_201); +lean_object* x_220; lean_object* x_221; +lean_dec(x_217); lean_dec(x_2); lean_dec(x_1); -x_204 = lean_box(1); -x_205 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_205, 0, x_204); -lean_ctor_set(x_205, 1, x_3); -return x_205; +x_220 = lean_box(1); +x_221 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_221, 0, x_220); +lean_ctor_set(x_221, 1, x_3); +return x_221; } else { -lean_object* x_206; lean_object* x_207; uint8_t x_208; -x_206 = l_Lean_Syntax_getArg(x_1, x_11); +lean_object* x_222; lean_object* x_223; uint8_t x_224; +x_222 = l_Lean_Syntax_getArg(x_1, x_11); lean_dec(x_1); lean_inc(x_2); -x_207 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(x_2, x_3); -x_208 = !lean_is_exclusive(x_207); -if (x_208 == 0) +x_223 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(x_2, x_3); +x_224 = !lean_is_exclusive(x_223); +if (x_224 == 0) { -lean_object* x_209; lean_object* x_210; lean_object* x_211; lean_object* x_212; lean_object* x_213; lean_object* x_214; lean_object* x_215; lean_object* x_216; lean_object* x_217; lean_object* x_218; lean_object* x_219; lean_object* x_220; lean_object* x_221; lean_object* x_222; lean_object* x_223; lean_object* x_224; lean_object* x_225; lean_object* x_226; lean_object* x_227; lean_object* x_228; lean_object* x_229; lean_object* x_230; lean_object* x_231; lean_object* x_232; lean_object* x_233; lean_object* x_234; lean_object* x_235; lean_object* x_236; lean_object* x_237; lean_object* x_238; lean_object* x_239; lean_object* x_240; lean_object* x_241; lean_object* x_242; lean_object* x_243; lean_object* x_244; lean_object* x_245; lean_object* x_246; lean_object* x_247; lean_object* x_248; lean_object* x_249; lean_object* x_250; lean_object* x_251; lean_object* x_252; lean_object* x_253; lean_object* x_254; lean_object* x_255; lean_object* x_256; lean_object* x_257; lean_object* x_258; lean_object* x_259; lean_object* x_260; lean_object* x_261; lean_object* x_262; lean_object* x_263; lean_object* x_264; lean_object* x_265; lean_object* x_266; lean_object* x_267; lean_object* x_268; lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274; lean_object* x_275; lean_object* x_276; lean_object* x_277; lean_object* x_278; lean_object* x_279; lean_object* x_280; lean_object* x_281; lean_object* x_282; lean_object* x_283; lean_object* x_284; lean_object* x_285; lean_object* x_286; lean_object* x_287; lean_object* x_288; lean_object* x_289; lean_object* x_290; lean_object* x_291; lean_object* x_292; lean_object* x_293; -x_209 = lean_ctor_get(x_207, 0); -x_210 = lean_ctor_get(x_2, 2); -lean_inc(x_210); -x_211 = lean_ctor_get(x_2, 1); -lean_inc(x_211); +lean_object* x_225; lean_object* x_226; lean_object* x_227; lean_object* x_228; lean_object* x_229; lean_object* x_230; lean_object* x_231; lean_object* x_232; lean_object* x_233; lean_object* x_234; lean_object* x_235; lean_object* x_236; lean_object* x_237; lean_object* x_238; lean_object* x_239; lean_object* x_240; lean_object* x_241; lean_object* x_242; lean_object* x_243; lean_object* x_244; lean_object* x_245; lean_object* x_246; lean_object* x_247; lean_object* x_248; lean_object* x_249; lean_object* x_250; lean_object* x_251; lean_object* x_252; lean_object* x_253; lean_object* x_254; lean_object* x_255; lean_object* x_256; lean_object* x_257; lean_object* x_258; lean_object* x_259; lean_object* x_260; lean_object* x_261; lean_object* x_262; lean_object* x_263; lean_object* x_264; lean_object* x_265; lean_object* x_266; lean_object* x_267; lean_object* x_268; lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274; lean_object* x_275; lean_object* x_276; lean_object* x_277; lean_object* x_278; lean_object* x_279; lean_object* x_280; lean_object* x_281; lean_object* x_282; lean_object* x_283; lean_object* x_284; lean_object* x_285; lean_object* x_286; lean_object* x_287; lean_object* x_288; lean_object* x_289; lean_object* x_290; lean_object* x_291; lean_object* x_292; lean_object* x_293; lean_object* x_294; lean_object* x_295; lean_object* x_296; lean_object* x_297; lean_object* x_298; lean_object* x_299; lean_object* x_300; lean_object* x_301; lean_object* x_302; lean_object* x_303; lean_object* x_304; lean_object* x_305; lean_object* x_306; lean_object* x_307; lean_object* x_308; lean_object* x_309; lean_object* x_310; lean_object* x_311; lean_object* x_312; lean_object* x_313; lean_object* x_314; lean_object* x_315; lean_object* x_316; lean_object* x_317; +x_225 = lean_ctor_get(x_223, 0); +x_226 = lean_ctor_get(x_2, 2); +lean_inc(x_226); +x_227 = lean_ctor_get(x_2, 1); +lean_inc(x_227); lean_dec(x_2); -x_212 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__7; -lean_inc(x_209); -x_213 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_213, 0, x_209); -lean_ctor_set(x_213, 1, x_212); -x_214 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__22; -lean_inc(x_210); -lean_inc(x_211); -x_215 = l_Lean_addMacroScope(x_211, x_214, x_210); -x_216 = lean_box(0); -x_217 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__21; -x_218 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__25; -lean_inc(x_209); -x_219 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_219, 0, x_209); -lean_ctor_set(x_219, 1, x_217); -lean_ctor_set(x_219, 2, x_215); -lean_ctor_set(x_219, 3, x_218); -x_220 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__26; -x_221 = lean_array_push(x_220, x_206); -x_222 = lean_box(2); -x_223 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__10; -x_224 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_224, 0, x_222); -lean_ctor_set(x_224, 1, x_223); -lean_ctor_set(x_224, 2, x_221); -x_225 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__27; -x_226 = lean_array_push(x_225, x_219); -x_227 = lean_array_push(x_226, x_224); -x_228 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__18; -x_229 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_229, 0, x_222); +x_228 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__7; +lean_inc(x_225); +x_229 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_229, 0, x_225); lean_ctor_set(x_229, 1, x_228); -lean_ctor_set(x_229, 2, x_227); -x_230 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__28; -x_231 = lean_array_push(x_230, x_229); -x_232 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__12; -x_233 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_233, 0, x_222); -lean_ctor_set(x_233, 1, x_232); -lean_ctor_set(x_233, 2, x_231); -x_234 = lean_array_push(x_220, x_233); -x_235 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_235, 0, x_222); -lean_ctor_set(x_235, 1, x_223); -lean_ctor_set(x_235, 2, x_234); -x_236 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__31; -lean_inc(x_209); -x_237 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_237, 0, x_209); -lean_ctor_set(x_237, 1, x_236); -x_238 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__34; -lean_inc(x_209); -x_239 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_239, 0, x_209); -lean_ctor_set(x_239, 1, x_238); -x_240 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__40; -lean_inc(x_210); -lean_inc(x_211); -x_241 = l_Lean_addMacroScope(x_211, x_240, x_210); -x_242 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__39; -lean_inc(x_209); -x_243 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_243, 0, x_209); -lean_ctor_set(x_243, 1, x_242); -lean_ctor_set(x_243, 2, x_241); -lean_ctor_set(x_243, 3, x_216); -x_244 = lean_array_push(x_230, x_243); -x_245 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__36; -x_246 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_246, 0, x_222); -lean_ctor_set(x_246, 1, x_245); -lean_ctor_set(x_246, 2, x_244); -x_247 = lean_array_push(x_220, x_201); -x_248 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_248, 0, x_222); -lean_ctor_set(x_248, 1, x_223); -lean_ctor_set(x_248, 2, x_247); -x_249 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__45; -lean_inc(x_209); -x_250 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_250, 0, x_209); -lean_ctor_set(x_250, 1, x_249); -x_251 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__48; -lean_inc(x_209); -x_252 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_252, 0, x_209); -lean_ctor_set(x_252, 1, x_251); -x_253 = lean_array_push(x_220, x_252); -x_254 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__47; -x_255 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_255, 0, x_222); +x_230 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__22; +lean_inc(x_226); +lean_inc(x_227); +x_231 = l_Lean_addMacroScope(x_227, x_230, x_226); +x_232 = lean_box(0); +x_233 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__21; +x_234 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__25; +lean_inc(x_225); +x_235 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_235, 0, x_225); +lean_ctor_set(x_235, 1, x_233); +lean_ctor_set(x_235, 2, x_231); +lean_ctor_set(x_235, 3, x_234); +x_236 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__26; +x_237 = lean_array_push(x_236, x_222); +x_238 = lean_box(2); +x_239 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__10; +x_240 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_240, 0, x_238); +lean_ctor_set(x_240, 1, x_239); +lean_ctor_set(x_240, 2, x_237); +x_241 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__27; +x_242 = lean_array_push(x_241, x_235); +x_243 = lean_array_push(x_242, x_240); +x_244 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__18; +x_245 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_245, 0, x_238); +lean_ctor_set(x_245, 1, x_244); +lean_ctor_set(x_245, 2, x_243); +x_246 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__28; +x_247 = lean_array_push(x_246, x_245); +x_248 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__12; +x_249 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_249, 0, x_238); +lean_ctor_set(x_249, 1, x_248); +lean_ctor_set(x_249, 2, x_247); +x_250 = lean_array_push(x_236, x_249); +x_251 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_251, 0, x_238); +lean_ctor_set(x_251, 1, x_239); +lean_ctor_set(x_251, 2, x_250); +x_252 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__31; +lean_inc(x_225); +x_253 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_253, 0, x_225); +lean_ctor_set(x_253, 1, x_252); +x_254 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__36; +lean_inc(x_225); +x_255 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_255, 0, x_225); lean_ctor_set(x_255, 1, x_254); -lean_ctor_set(x_255, 2, x_253); -x_256 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__49; -x_257 = lean_array_push(x_256, x_239); -lean_inc(x_257); -x_258 = lean_array_push(x_257, x_246); -lean_inc(x_248); -x_259 = lean_array_push(x_258, x_248); -lean_inc(x_250); -x_260 = lean_array_push(x_259, x_250); -lean_inc(x_255); -x_261 = lean_array_push(x_260, x_255); -x_262 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__33; -x_263 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_263, 0, x_222); -lean_ctor_set(x_263, 1, x_262); -lean_ctor_set(x_263, 2, x_261); -x_264 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__53; -x_265 = l_Lean_addMacroScope(x_211, x_264, x_210); -x_266 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__52; -x_267 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_267, 0, x_209); -lean_ctor_set(x_267, 1, x_266); -lean_ctor_set(x_267, 2, x_265); -lean_ctor_set(x_267, 3, x_216); -x_268 = lean_array_push(x_230, x_267); -x_269 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_269, 0, x_222); -lean_ctor_set(x_269, 1, x_245); -lean_ctor_set(x_269, 2, x_268); -x_270 = lean_array_push(x_257, x_269); -x_271 = lean_array_push(x_270, x_248); -x_272 = lean_array_push(x_271, x_250); -x_273 = lean_array_push(x_272, x_255); -x_274 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_274, 0, x_222); -lean_ctor_set(x_274, 1, x_262); -lean_ctor_set(x_274, 2, x_273); -x_275 = lean_array_push(x_225, x_263); -x_276 = lean_array_push(x_275, x_274); -x_277 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_277, 0, x_222); -lean_ctor_set(x_277, 1, x_223); -lean_ctor_set(x_277, 2, x_276); -x_278 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54; -x_279 = lean_array_push(x_278, x_237); -x_280 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__14; -x_281 = lean_array_push(x_279, x_280); -x_282 = lean_array_push(x_281, x_277); -x_283 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__30; +x_256 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__42; +lean_inc(x_226); +lean_inc(x_227); +x_257 = l_Lean_addMacroScope(x_227, x_256, x_226); +x_258 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__41; +lean_inc(x_225); +x_259 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_259, 0, x_225); +lean_ctor_set(x_259, 1, x_258); +lean_ctor_set(x_259, 2, x_257); +lean_ctor_set(x_259, 3, x_232); +x_260 = lean_array_push(x_246, x_259); +x_261 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__38; +x_262 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_262, 0, x_238); +lean_ctor_set(x_262, 1, x_261); +lean_ctor_set(x_262, 2, x_260); +x_263 = lean_array_push(x_236, x_217); +x_264 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_264, 0, x_238); +lean_ctor_set(x_264, 1, x_239); +lean_ctor_set(x_264, 2, x_263); +x_265 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__47; +x_266 = lean_array_push(x_265, x_255); +lean_inc(x_266); +x_267 = lean_array_push(x_266, x_262); +lean_inc(x_264); +x_268 = lean_array_push(x_267, x_264); +x_269 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__35; +x_270 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_270, 0, x_238); +lean_ctor_set(x_270, 1, x_269); +lean_ctor_set(x_270, 2, x_268); +x_271 = lean_array_push(x_236, x_270); +x_272 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_272, 0, x_238); +lean_ctor_set(x_272, 1, x_239); +lean_ctor_set(x_272, 2, x_271); +x_273 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__48; +lean_inc(x_225); +x_274 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_274, 0, x_225); +lean_ctor_set(x_274, 1, x_273); +x_275 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__51; +lean_inc(x_225); +x_276 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_276, 0, x_225); +lean_ctor_set(x_276, 1, x_275); +x_277 = lean_array_push(x_236, x_276); +x_278 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__50; +x_279 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_279, 0, x_238); +lean_ctor_set(x_279, 1, x_278); +lean_ctor_set(x_279, 2, x_277); +x_280 = lean_array_push(x_265, x_272); +lean_inc(x_274); +x_281 = lean_array_push(x_280, x_274); +lean_inc(x_279); +x_282 = lean_array_push(x_281, x_279); +x_283 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__33; x_284 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_284, 0, x_222); +lean_ctor_set(x_284, 0, x_238); lean_ctor_set(x_284, 1, x_283); lean_ctor_set(x_284, 2, x_282); -x_285 = lean_array_push(x_220, x_284); -x_286 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_286, 0, x_222); -lean_ctor_set(x_286, 1, x_223); -lean_ctor_set(x_286, 2, x_285); -x_287 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55; -x_288 = lean_array_push(x_287, x_213); -x_289 = lean_array_push(x_288, x_235); -x_290 = lean_array_push(x_289, x_280); -x_291 = lean_array_push(x_290, x_286); -x_292 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__8; +x_285 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55; +x_286 = l_Lean_addMacroScope(x_227, x_285, x_226); +x_287 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54; +x_288 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_288, 0, x_225); +lean_ctor_set(x_288, 1, x_287); +lean_ctor_set(x_288, 2, x_286); +lean_ctor_set(x_288, 3, x_232); +x_289 = lean_array_push(x_246, x_288); +x_290 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_290, 0, x_238); +lean_ctor_set(x_290, 1, x_261); +lean_ctor_set(x_290, 2, x_289); +x_291 = lean_array_push(x_266, x_290); +x_292 = lean_array_push(x_291, x_264); x_293 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_293, 0, x_222); -lean_ctor_set(x_293, 1, x_292); -lean_ctor_set(x_293, 2, x_291); -lean_ctor_set(x_207, 0, x_293); -return x_207; +lean_ctor_set(x_293, 0, x_238); +lean_ctor_set(x_293, 1, x_269); +lean_ctor_set(x_293, 2, x_292); +x_294 = lean_array_push(x_236, x_293); +x_295 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_295, 0, x_238); +lean_ctor_set(x_295, 1, x_239); +lean_ctor_set(x_295, 2, x_294); +x_296 = lean_array_push(x_265, x_295); +x_297 = lean_array_push(x_296, x_274); +x_298 = lean_array_push(x_297, x_279); +x_299 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_299, 0, x_238); +lean_ctor_set(x_299, 1, x_283); +lean_ctor_set(x_299, 2, x_298); +x_300 = lean_array_push(x_241, x_284); +x_301 = lean_array_push(x_300, x_299); +x_302 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_302, 0, x_238); +lean_ctor_set(x_302, 1, x_239); +lean_ctor_set(x_302, 2, x_301); +x_303 = lean_array_push(x_265, x_253); +x_304 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__14; +x_305 = lean_array_push(x_303, x_304); +x_306 = lean_array_push(x_305, x_302); +x_307 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__30; +x_308 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_308, 0, x_238); +lean_ctor_set(x_308, 1, x_307); +lean_ctor_set(x_308, 2, x_306); +x_309 = lean_array_push(x_236, x_308); +x_310 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_310, 0, x_238); +lean_ctor_set(x_310, 1, x_239); +lean_ctor_set(x_310, 2, x_309); +x_311 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__56; +x_312 = lean_array_push(x_311, x_229); +x_313 = lean_array_push(x_312, x_251); +x_314 = lean_array_push(x_313, x_304); +x_315 = lean_array_push(x_314, x_310); +x_316 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__8; +x_317 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_317, 0, x_238); +lean_ctor_set(x_317, 1, x_316); +lean_ctor_set(x_317, 2, x_315); +lean_ctor_set(x_223, 0, x_317); +return x_223; } else { -lean_object* x_294; lean_object* x_295; lean_object* x_296; lean_object* x_297; lean_object* x_298; lean_object* x_299; lean_object* x_300; lean_object* x_301; lean_object* x_302; lean_object* x_303; lean_object* x_304; lean_object* x_305; lean_object* x_306; lean_object* x_307; lean_object* x_308; lean_object* x_309; lean_object* x_310; lean_object* x_311; lean_object* x_312; lean_object* x_313; lean_object* x_314; lean_object* x_315; lean_object* x_316; lean_object* x_317; lean_object* x_318; lean_object* x_319; lean_object* x_320; lean_object* x_321; lean_object* x_322; lean_object* x_323; lean_object* x_324; lean_object* x_325; lean_object* x_326; lean_object* x_327; lean_object* x_328; lean_object* x_329; lean_object* x_330; lean_object* x_331; lean_object* x_332; lean_object* x_333; lean_object* x_334; lean_object* x_335; lean_object* x_336; lean_object* x_337; lean_object* x_338; lean_object* x_339; lean_object* x_340; lean_object* x_341; lean_object* x_342; lean_object* x_343; lean_object* x_344; lean_object* x_345; lean_object* x_346; lean_object* x_347; lean_object* x_348; lean_object* x_349; lean_object* x_350; lean_object* x_351; lean_object* x_352; lean_object* x_353; lean_object* x_354; lean_object* x_355; lean_object* x_356; lean_object* x_357; lean_object* x_358; lean_object* x_359; lean_object* x_360; lean_object* x_361; lean_object* x_362; lean_object* x_363; lean_object* x_364; lean_object* x_365; lean_object* x_366; lean_object* x_367; lean_object* x_368; lean_object* x_369; lean_object* x_370; lean_object* x_371; lean_object* x_372; lean_object* x_373; lean_object* x_374; lean_object* x_375; lean_object* x_376; lean_object* x_377; lean_object* x_378; lean_object* x_379; lean_object* x_380; -x_294 = lean_ctor_get(x_207, 0); -x_295 = lean_ctor_get(x_207, 1); -lean_inc(x_295); -lean_inc(x_294); -lean_dec(x_207); -x_296 = lean_ctor_get(x_2, 2); -lean_inc(x_296); -x_297 = lean_ctor_get(x_2, 1); -lean_inc(x_297); +lean_object* x_318; lean_object* x_319; lean_object* x_320; lean_object* x_321; lean_object* x_322; lean_object* x_323; lean_object* x_324; lean_object* x_325; lean_object* x_326; lean_object* x_327; lean_object* x_328; lean_object* x_329; lean_object* x_330; lean_object* x_331; lean_object* x_332; lean_object* x_333; lean_object* x_334; lean_object* x_335; lean_object* x_336; lean_object* x_337; lean_object* x_338; lean_object* x_339; lean_object* x_340; lean_object* x_341; lean_object* x_342; lean_object* x_343; lean_object* x_344; lean_object* x_345; lean_object* x_346; lean_object* x_347; lean_object* x_348; lean_object* x_349; lean_object* x_350; lean_object* x_351; lean_object* x_352; lean_object* x_353; lean_object* x_354; lean_object* x_355; lean_object* x_356; lean_object* x_357; lean_object* x_358; lean_object* x_359; lean_object* x_360; lean_object* x_361; lean_object* x_362; lean_object* x_363; lean_object* x_364; lean_object* x_365; lean_object* x_366; lean_object* x_367; lean_object* x_368; lean_object* x_369; lean_object* x_370; lean_object* x_371; lean_object* x_372; lean_object* x_373; lean_object* x_374; lean_object* x_375; lean_object* x_376; lean_object* x_377; lean_object* x_378; lean_object* x_379; lean_object* x_380; lean_object* x_381; lean_object* x_382; lean_object* x_383; lean_object* x_384; lean_object* x_385; lean_object* x_386; lean_object* x_387; lean_object* x_388; lean_object* x_389; lean_object* x_390; lean_object* x_391; lean_object* x_392; lean_object* x_393; lean_object* x_394; lean_object* x_395; lean_object* x_396; lean_object* x_397; lean_object* x_398; lean_object* x_399; lean_object* x_400; lean_object* x_401; lean_object* x_402; lean_object* x_403; lean_object* x_404; lean_object* x_405; lean_object* x_406; lean_object* x_407; lean_object* x_408; lean_object* x_409; lean_object* x_410; lean_object* x_411; lean_object* x_412; +x_318 = lean_ctor_get(x_223, 0); +x_319 = lean_ctor_get(x_223, 1); +lean_inc(x_319); +lean_inc(x_318); +lean_dec(x_223); +x_320 = lean_ctor_get(x_2, 2); +lean_inc(x_320); +x_321 = lean_ctor_get(x_2, 1); +lean_inc(x_321); lean_dec(x_2); -x_298 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__7; -lean_inc(x_294); -x_299 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_299, 0, x_294); -lean_ctor_set(x_299, 1, x_298); -x_300 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__22; -lean_inc(x_296); -lean_inc(x_297); -x_301 = l_Lean_addMacroScope(x_297, x_300, x_296); -x_302 = lean_box(0); -x_303 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__21; -x_304 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__25; -lean_inc(x_294); -x_305 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_305, 0, x_294); -lean_ctor_set(x_305, 1, x_303); -lean_ctor_set(x_305, 2, x_301); -lean_ctor_set(x_305, 3, x_304); -x_306 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__26; -x_307 = lean_array_push(x_306, x_206); -x_308 = lean_box(2); -x_309 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__10; -x_310 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_310, 0, x_308); -lean_ctor_set(x_310, 1, x_309); -lean_ctor_set(x_310, 2, x_307); -x_311 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__27; -x_312 = lean_array_push(x_311, x_305); -x_313 = lean_array_push(x_312, x_310); -x_314 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__18; -x_315 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_315, 0, x_308); -lean_ctor_set(x_315, 1, x_314); -lean_ctor_set(x_315, 2, x_313); -x_316 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__28; -x_317 = lean_array_push(x_316, x_315); -x_318 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__12; -x_319 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_319, 0, x_308); -lean_ctor_set(x_319, 1, x_318); -lean_ctor_set(x_319, 2, x_317); -x_320 = lean_array_push(x_306, x_319); -x_321 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_321, 0, x_308); -lean_ctor_set(x_321, 1, x_309); -lean_ctor_set(x_321, 2, x_320); -x_322 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__31; -lean_inc(x_294); +x_322 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__7; +lean_inc(x_318); x_323 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_323, 0, x_294); +lean_ctor_set(x_323, 0, x_318); lean_ctor_set(x_323, 1, x_322); -x_324 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__34; -lean_inc(x_294); -x_325 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_325, 0, x_294); -lean_ctor_set(x_325, 1, x_324); -x_326 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__40; -lean_inc(x_296); -lean_inc(x_297); -x_327 = l_Lean_addMacroScope(x_297, x_326, x_296); -x_328 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__39; -lean_inc(x_294); +x_324 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__22; +lean_inc(x_320); +lean_inc(x_321); +x_325 = l_Lean_addMacroScope(x_321, x_324, x_320); +x_326 = lean_box(0); +x_327 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__21; +x_328 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__25; +lean_inc(x_318); x_329 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_329, 0, x_294); -lean_ctor_set(x_329, 1, x_328); -lean_ctor_set(x_329, 2, x_327); -lean_ctor_set(x_329, 3, x_302); -x_330 = lean_array_push(x_316, x_329); -x_331 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__36; -x_332 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_332, 0, x_308); -lean_ctor_set(x_332, 1, x_331); -lean_ctor_set(x_332, 2, x_330); -x_333 = lean_array_push(x_306, x_201); +lean_ctor_set(x_329, 0, x_318); +lean_ctor_set(x_329, 1, x_327); +lean_ctor_set(x_329, 2, x_325); +lean_ctor_set(x_329, 3, x_328); +x_330 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__26; +x_331 = lean_array_push(x_330, x_222); +x_332 = lean_box(2); +x_333 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__10; x_334 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_334, 0, x_308); -lean_ctor_set(x_334, 1, x_309); -lean_ctor_set(x_334, 2, x_333); -x_335 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__45; -lean_inc(x_294); -x_336 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_336, 0, x_294); -lean_ctor_set(x_336, 1, x_335); -x_337 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__48; -lean_inc(x_294); -x_338 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_338, 0, x_294); -lean_ctor_set(x_338, 1, x_337); -x_339 = lean_array_push(x_306, x_338); -x_340 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__47; -x_341 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_341, 0, x_308); -lean_ctor_set(x_341, 1, x_340); -lean_ctor_set(x_341, 2, x_339); -x_342 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__49; -x_343 = lean_array_push(x_342, x_325); -lean_inc(x_343); -x_344 = lean_array_push(x_343, x_332); -lean_inc(x_334); -x_345 = lean_array_push(x_344, x_334); -lean_inc(x_336); -x_346 = lean_array_push(x_345, x_336); -lean_inc(x_341); -x_347 = lean_array_push(x_346, x_341); -x_348 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__33; -x_349 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_349, 0, x_308); +lean_ctor_set(x_334, 0, x_332); +lean_ctor_set(x_334, 1, x_333); +lean_ctor_set(x_334, 2, x_331); +x_335 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__27; +x_336 = lean_array_push(x_335, x_329); +x_337 = lean_array_push(x_336, x_334); +x_338 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__18; +x_339 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_339, 0, x_332); +lean_ctor_set(x_339, 1, x_338); +lean_ctor_set(x_339, 2, x_337); +x_340 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__28; +x_341 = lean_array_push(x_340, x_339); +x_342 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__12; +x_343 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_343, 0, x_332); +lean_ctor_set(x_343, 1, x_342); +lean_ctor_set(x_343, 2, x_341); +x_344 = lean_array_push(x_330, x_343); +x_345 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_345, 0, x_332); +lean_ctor_set(x_345, 1, x_333); +lean_ctor_set(x_345, 2, x_344); +x_346 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__31; +lean_inc(x_318); +x_347 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_347, 0, x_318); +lean_ctor_set(x_347, 1, x_346); +x_348 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__36; +lean_inc(x_318); +x_349 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_349, 0, x_318); lean_ctor_set(x_349, 1, x_348); -lean_ctor_set(x_349, 2, x_347); -x_350 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__53; -x_351 = l_Lean_addMacroScope(x_297, x_350, x_296); -x_352 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__52; +x_350 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__42; +lean_inc(x_320); +lean_inc(x_321); +x_351 = l_Lean_addMacroScope(x_321, x_350, x_320); +x_352 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__41; +lean_inc(x_318); x_353 = lean_alloc_ctor(3, 4, 0); -lean_ctor_set(x_353, 0, x_294); +lean_ctor_set(x_353, 0, x_318); lean_ctor_set(x_353, 1, x_352); lean_ctor_set(x_353, 2, x_351); -lean_ctor_set(x_353, 3, x_302); -x_354 = lean_array_push(x_316, x_353); -x_355 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_355, 0, x_308); -lean_ctor_set(x_355, 1, x_331); -lean_ctor_set(x_355, 2, x_354); -x_356 = lean_array_push(x_343, x_355); -x_357 = lean_array_push(x_356, x_334); -x_358 = lean_array_push(x_357, x_336); -x_359 = lean_array_push(x_358, x_341); -x_360 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_360, 0, x_308); -lean_ctor_set(x_360, 1, x_348); -lean_ctor_set(x_360, 2, x_359); -x_361 = lean_array_push(x_311, x_349); -x_362 = lean_array_push(x_361, x_360); -x_363 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_363, 0, x_308); -lean_ctor_set(x_363, 1, x_309); -lean_ctor_set(x_363, 2, x_362); -x_364 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54; -x_365 = lean_array_push(x_364, x_323); -x_366 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__14; -x_367 = lean_array_push(x_365, x_366); -x_368 = lean_array_push(x_367, x_363); -x_369 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__30; -x_370 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_370, 0, x_308); +lean_ctor_set(x_353, 3, x_326); +x_354 = lean_array_push(x_340, x_353); +x_355 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__38; +x_356 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_356, 0, x_332); +lean_ctor_set(x_356, 1, x_355); +lean_ctor_set(x_356, 2, x_354); +x_357 = lean_array_push(x_330, x_217); +x_358 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_358, 0, x_332); +lean_ctor_set(x_358, 1, x_333); +lean_ctor_set(x_358, 2, x_357); +x_359 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__47; +x_360 = lean_array_push(x_359, x_349); +lean_inc(x_360); +x_361 = lean_array_push(x_360, x_356); +lean_inc(x_358); +x_362 = lean_array_push(x_361, x_358); +x_363 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__35; +x_364 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_364, 0, x_332); +lean_ctor_set(x_364, 1, x_363); +lean_ctor_set(x_364, 2, x_362); +x_365 = lean_array_push(x_330, x_364); +x_366 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_366, 0, x_332); +lean_ctor_set(x_366, 1, x_333); +lean_ctor_set(x_366, 2, x_365); +x_367 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__48; +lean_inc(x_318); +x_368 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_368, 0, x_318); +lean_ctor_set(x_368, 1, x_367); +x_369 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__51; +lean_inc(x_318); +x_370 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_370, 0, x_318); lean_ctor_set(x_370, 1, x_369); -lean_ctor_set(x_370, 2, x_368); -x_371 = lean_array_push(x_306, x_370); -x_372 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_372, 0, x_308); -lean_ctor_set(x_372, 1, x_309); -lean_ctor_set(x_372, 2, x_371); -x_373 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55; -x_374 = lean_array_push(x_373, x_299); -x_375 = lean_array_push(x_374, x_321); -x_376 = lean_array_push(x_375, x_366); -x_377 = lean_array_push(x_376, x_372); -x_378 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__8; -x_379 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_379, 0, x_308); -lean_ctor_set(x_379, 1, x_378); -lean_ctor_set(x_379, 2, x_377); -x_380 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_380, 0, x_379); -lean_ctor_set(x_380, 1, x_295); -return x_380; +x_371 = lean_array_push(x_330, x_370); +x_372 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__50; +x_373 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_373, 0, x_332); +lean_ctor_set(x_373, 1, x_372); +lean_ctor_set(x_373, 2, x_371); +x_374 = lean_array_push(x_359, x_366); +lean_inc(x_368); +x_375 = lean_array_push(x_374, x_368); +lean_inc(x_373); +x_376 = lean_array_push(x_375, x_373); +x_377 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__33; +x_378 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_378, 0, x_332); +lean_ctor_set(x_378, 1, x_377); +lean_ctor_set(x_378, 2, x_376); +x_379 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55; +x_380 = l_Lean_addMacroScope(x_321, x_379, x_320); +x_381 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54; +x_382 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_382, 0, x_318); +lean_ctor_set(x_382, 1, x_381); +lean_ctor_set(x_382, 2, x_380); +lean_ctor_set(x_382, 3, x_326); +x_383 = lean_array_push(x_340, x_382); +x_384 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_384, 0, x_332); +lean_ctor_set(x_384, 1, x_355); +lean_ctor_set(x_384, 2, x_383); +x_385 = lean_array_push(x_360, x_384); +x_386 = lean_array_push(x_385, x_358); +x_387 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_387, 0, x_332); +lean_ctor_set(x_387, 1, x_363); +lean_ctor_set(x_387, 2, x_386); +x_388 = lean_array_push(x_330, x_387); +x_389 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_389, 0, x_332); +lean_ctor_set(x_389, 1, x_333); +lean_ctor_set(x_389, 2, x_388); +x_390 = lean_array_push(x_359, x_389); +x_391 = lean_array_push(x_390, x_368); +x_392 = lean_array_push(x_391, x_373); +x_393 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_393, 0, x_332); +lean_ctor_set(x_393, 1, x_377); +lean_ctor_set(x_393, 2, x_392); +x_394 = lean_array_push(x_335, x_378); +x_395 = lean_array_push(x_394, x_393); +x_396 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_396, 0, x_332); +lean_ctor_set(x_396, 1, x_333); +lean_ctor_set(x_396, 2, x_395); +x_397 = lean_array_push(x_359, x_347); +x_398 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__14; +x_399 = lean_array_push(x_397, x_398); +x_400 = lean_array_push(x_399, x_396); +x_401 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__30; +x_402 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_402, 0, x_332); +lean_ctor_set(x_402, 1, x_401); +lean_ctor_set(x_402, 2, x_400); +x_403 = lean_array_push(x_330, x_402); +x_404 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_404, 0, x_332); +lean_ctor_set(x_404, 1, x_333); +lean_ctor_set(x_404, 2, x_403); +x_405 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__56; +x_406 = lean_array_push(x_405, x_323); +x_407 = lean_array_push(x_406, x_345); +x_408 = lean_array_push(x_407, x_398); +x_409 = lean_array_push(x_408, x_404); +x_410 = l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__8; +x_411 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_411, 0, x_332); +lean_ctor_set(x_411, 1, x_410); +lean_ctor_set(x_411, 2, x_409); +x_412 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_412, 0, x_411); +lean_ctor_set(x_412, 1, x_319); +return x_412; } } } @@ -1894,6 +1984,8 @@ l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases__ lean_mark_persistent(l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__54); l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55 = _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55(); lean_mark_persistent(l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__55); +l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__56 = _init_l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__56(); +lean_mark_persistent(l_Classical___aux__Init__Classical______macroRules__Classical__tacticBy__cases_____x3a____1___closed__56); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Init/Tactics.c b/stage0/stdlib/Init/Tactics.c index 1df2e57bf4..ce362d040d 100644 --- a/stage0/stdlib/Init/Tactics.c +++ b/stage0/stdlib/Init/Tactics.c @@ -126,9 +126,11 @@ static lean_object* l_Lean_Parser_Tactic_intro___closed__4; static lean_object* l_Lean_Parser_Tactic_simp___closed__10; static lean_object* l_term_u2039___u203a___closed__3; static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRfl_x27__1___closed__3; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__11; static lean_object* l_Lean_Parser_Tactic_rwRuleSeq___closed__2; static lean_object* l_term_u2039___u203a___closed__5; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticRfl_x27; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__12; static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRfl_x27__1___closed__5; static lean_object* l_Lean_Parser_Tactic_simpPost___closed__2; static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__8; @@ -168,12 +170,13 @@ static lean_object* l_Lean_Parser_Tactic_withAnnotateState___closed__19; static lean_object* l_Lean_Parser_Tactic_tacticStop_____closed__7; static lean_object* l_Lean_Parser_Tactic_injection___closed__8; static lean_object* l_Lean_Parser_Tactic_changeWith___closed__5; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__13; static lean_object* l_Lean_Parser_Tactic_rwSeq___closed__1; -static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__27; static lean_object* l_Lean_Parser_Tactic_tacticInfer__instance___closed__3; static lean_object* l_Lean_Parser_Tactic_apply___closed__4; static lean_object* l_Lean_Parser_Tactic_casesTarget___closed__4; static lean_object* l_Lean_Parser_Tactic_tacticHave_____closed__3; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__6; static lean_object* l_Lean_Parser_Tactic_unfold___closed__4; static lean_object* l_Lean_Parser_Tactic_change___closed__1; static lean_object* l_Lean_Parser_Tactic_tacticRefine__lift_____closed__5; @@ -188,7 +191,6 @@ static lean_object* l_Lean_Parser_Tactic_dsimp___closed__9; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticExists___x2c_x2c__1(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_Tactic_tacticTrivial___closed__4; static lean_object* l_Lean_Parser_Tactic_case___closed__11; -static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__24; static lean_object* l_Lean_Parser_Tactic_tacticLet_____closed__4; static lean_object* l_Lean_Parser_Tactic_unfold___closed__8; static lean_object* l_Lean_Parser_Tactic_refl___closed__4; @@ -287,6 +289,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_contradiction; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticLet_x27____1(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_Tactic_clear___closed__1; static lean_object* l_Lean_Parser_Tactic_withUnfoldingAll___closed__2; +LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_inductionAltLHS; static lean_object* l_Lean_Parser_Tactic_clear___closed__2; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_clear; static lean_object* l_Lean_Parser_Tactic_withReducibleAndInstances___closed__6; @@ -357,6 +360,7 @@ static lean_object* l_Lean_Parser_Tactic_intros___closed__8; static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticTrivial__5___closed__3; static lean_object* l_Lean_Parser_Tactic_split___closed__1; static lean_object* l_Lean_Parser_Attr_simp___closed__7; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__10; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_unfold; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticHave__; static lean_object* l_Lean_Parser_Attr_simp___closed__3; @@ -414,7 +418,6 @@ static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__L static lean_object* l_Lean_Parser_Tactic_dsimp___closed__8; static lean_object* l_Lean_Parser_Tactic_tacticAdmit___closed__5; static lean_object* l_Lean_Parser_Tactic_withUnfoldingAll___closed__4; -static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__20; static lean_object* l_Lean_Parser_Tactic_changeWith___closed__8; static lean_object* l_Lean_Parser_Tactic_focus___closed__1; static lean_object* l_Lean_Parser_Tactic_tacticSuffices_____closed__4; @@ -581,7 +584,6 @@ static lean_object* l_Lean_Parser_Tactic_simpStar___closed__1; static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__14; static lean_object* l_Lean_Parser_Tactic_tacticLet_x27_____closed__5; static lean_object* l_Lean_Parser_Tactic_case_x27___closed__8; -static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__28; static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticTrivial__4___closed__2; static lean_object* l_Lean_Parser_Tactic_refine___closed__6; static lean_object* l_Lean_Parser_Tactic_tacticHave_____closed__8; @@ -668,7 +670,6 @@ static lean_object* l_Lean_Parser_Tactic_rewriteSeq___closed__6; static lean_object* l_Lean_Parser_Tactic_first___closed__10; static lean_object* l_Lean_Parser_Tactic_ac__refl___closed__4; static lean_object* l_Lean_Parser_Tactic_intros___closed__9; -static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__22; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticSorry__1(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_Tactic_sleep___closed__4; static lean_object* l_Lean_Parser_Tactic_tacticHave_x27_____x3a_x3d_____closed__2; @@ -813,7 +814,7 @@ static lean_object* l_Lean_Parser_Tactic_withAnnotateState___closed__4; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRfl_x27__1(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRfl_x27__1___closed__4; static lean_object* l_Lean_Parser_Tactic_rwRule___closed__1; -static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__23; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__4; static lean_object* l_Lean_Parser_Tactic_tacticHave_____x3a_x3d_____closed__2; static lean_object* l_Lean_Parser_Tactic_split___closed__9; static lean_object* l_Lean_Parser_Tactic_intro___closed__6; @@ -824,6 +825,7 @@ static lean_object* l_Lean_Parser_Tactic_tacticSorry___closed__4; static lean_object* l_Lean_Parser_Tactic_cases___closed__7; static lean_object* l_Lean_Parser_Tactic_tacticTry_____closed__2; static lean_object* l_Lean_Parser_Tactic_rewriteSeq___closed__5; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__8; static lean_object* l_term_u2039___u203a___closed__9; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_simpPost; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_done; @@ -832,7 +834,6 @@ static lean_object* l_Lean_Parser_Tactic_withAnnotateState___closed__17; static lean_object* l_Lean_Parser_Tactic_tacticRfl_x27___closed__2; static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRefine__lift____1___closed__1; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_intros; -static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__21; static lean_object* l_Lean_Parser_Tactic_rewriteSeq___closed__3; static lean_object* l_Lean_Parser_Tactic_tactic___x3c_x3b_x3e_____closed__6; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticTry__; @@ -876,6 +877,7 @@ uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*); static lean_object* l_Lean_Parser_Tactic_renameI___closed__6; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticStop__; static lean_object* l_Lean_Parser_Tactic_induction___closed__4; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__2; static lean_object* l_Lean_Parser_Tactic_rotateLeft___closed__11; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_anyGoals; static lean_object* l_Lean_Parser_Tactic_tacticRepeat_____closed__1; @@ -920,6 +922,7 @@ static lean_object* l_Lean_Parser_Tactic_fail___closed__5; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_discharger; static lean_object* l_Lean_Parser_Tactic_withAnnotateState___closed__8; lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*); +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__9; LEAN_EXPORT lean_object* l_term_u2039___u203a; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_withUnfoldingAll; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticTry____1(lean_object*, lean_object*, lean_object*); @@ -950,6 +953,7 @@ static lean_object* l_Lean_Parser_Tactic_inductionAlts___closed__1; static lean_object* l_Lean_Parser_Tactic_simpErase___closed__3; static lean_object* l___aux__Init__Tactics______macroRules__term_u2039___u203a__1___closed__2; static lean_object* l_Lean_Parser_Tactic_withAnnotateState___closed__21; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__3; static lean_object* l_Lean_Parser_Tactic_contradiction___closed__4; static lean_object* l_Lean_Parser_Tactic_rwSeq___closed__3; static lean_object* l_Lean_Parser_Tactic_tacticHave_x27_____closed__4; @@ -973,7 +977,6 @@ static lean_object* l_Lean_Parser_Tactic_induction___closed__17; static lean_object* l_Lean_Parser_Tactic_withAnnotateState___closed__13; static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticNext_______x3d_x3e____1___closed__4; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_casesTarget; -static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__25; static lean_object* l_Lean_Parser_Tactic_letrec___closed__3; static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticHave_____x3a_x3d____1___closed__3; static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticInfer__instance__1___closed__4; @@ -991,7 +994,6 @@ static lean_object* l_Lean_Parser_Attr_simp___closed__1; static lean_object* l_Lean_Parser_Tactic_rwRule___closed__3; static lean_object* l_Lean_Parser_Tactic_simp___closed__16; static lean_object* l_Lean_Parser_Tactic_casesTarget___closed__2; -static lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__26; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticShow__; static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticTrivial__5___closed__2; static lean_object* l_Lean_Parser_Tactic_rename___closed__6; @@ -1000,6 +1002,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_expandRwSeq(lean_object*, lean_obj static lean_object* l_Lean_Parser_Tactic_tacticRefine__lift_____closed__1; static lean_object* l_Lean_Parser_Tactic_rotateLeft___closed__9; static lean_object* l_Lean_Parser_Tactic_allGoals___closed__1; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__1; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_traceState; LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_rotateRight; static lean_object* l_Lean_Parser_Tactic_intro___closed__15; @@ -1041,6 +1044,7 @@ static lean_object* l_term_u2039___u203a___closed__4; static lean_object* l_Lean_Parser_Tactic_rwWithRfl___closed__1; static lean_object* l_Lean_Parser_Tactic_rewriteSeq___closed__2; static lean_object* l_Lean_Parser_Tactic_dbgTrace___closed__1; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__7; static lean_object* l_Lean_Parser_Attr_simp___closed__9; static lean_object* l_Lean_Parser_Tactic_letrec___closed__10; static lean_object* l_Lean_Parser_Tactic_withAnnotateState___closed__23; @@ -1049,6 +1053,7 @@ static lean_object* l_Lean_Parser_Tactic_tacticAdmit___closed__4; static lean_object* l_Lean_Parser_Tactic_refine_x27___closed__1; static lean_object* l_Lean_Parser_Tactic_specialize___closed__4; static lean_object* l_Lean_Parser_Attr_simp___closed__4; +static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__5; static lean_object* l_Lean_Parser_Tactic_intros___closed__10; static lean_object* l_Lean_Parser_Tactic_refine_x27___closed__2; static lean_object* l_Lean_Parser_Tactic_tactic___x3c_x3b_x3e_____closed__3; @@ -13221,6 +13226,162 @@ return x_93; } } } +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("inductionAltLHS", 15); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__6; +x_2 = l_Lean_Parser_Tactic_inductionAltLHS___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("| ", 2); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Tactic_inductionAltLHS___closed__3; +x_2 = lean_alloc_ctor(5, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_from_bytes("@", 1); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Tactic_inductionAltLHS___closed__5; +x_2 = lean_alloc_ctor(5, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_rotateLeft___closed__6; +x_2 = l_Lean_Parser_Tactic_inductionAltLHS___closed__6; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__8() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__10; +x_2 = l_Lean_Parser_Tactic_inductionAltLHS___closed__7; +x_3 = l_Lean_Parser_Tactic_intros___closed__9; +x_4 = lean_alloc_ctor(2, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__9() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_first___closed__8; +x_2 = l_Lean_Parser_Tactic_inductionAltLHS___closed__8; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__10() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_intros___closed__6; +x_2 = l_Lean_Parser_Tactic_inductionAltLHS___closed__9; +x_3 = l_Lean_Parser_Tactic_intros___closed__11; +x_4 = lean_alloc_ctor(2, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__11() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__10; +x_2 = l_Lean_Parser_Tactic_inductionAltLHS___closed__4; +x_3 = l_Lean_Parser_Tactic_inductionAltLHS___closed__10; +x_4 = lean_alloc_ctor(2, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__12() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__10; +x_2 = l_Lean_Parser_Tactic_inductionAltLHS___closed__11; +x_3 = l_Lean_Parser_Tactic_tacticNext_______x3d_x3e_____closed__5; +x_4 = lean_alloc_ctor(2, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__13() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_inductionAltLHS___closed__1; +x_2 = l_Lean_Parser_Tactic_inductionAltLHS___closed__2; +x_3 = l_Lean_Parser_Tactic_inductionAltLHS___closed__12; +x_4 = lean_alloc_ctor(9, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAltLHS() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_Tactic_inductionAltLHS___closed__13; +return x_1; +} +} static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__1() { _start: { @@ -13300,19 +13461,27 @@ return x_3; static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__9() { _start: { -lean_object* x_1; -x_1 = lean_mk_string_from_bytes("| ", 2); -return x_1; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_revert___closed__6; +x_2 = l_Lean_Parser_Tactic_inductionAltLHS; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; } } static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__10() { _start: { -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__9; -x_2 = lean_alloc_ctor(5, 1, 0); -lean_ctor_set(x_2, 0, x_1); -return x_2; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__10; +x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__8; +x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__9; +x_4 = lean_alloc_ctor(2, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; } } static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__11() { @@ -13320,8 +13489,8 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__10; -x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__8; -x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__10; +x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__10; +x_3 = l_Lean_Parser_Tactic_rename___closed__8; x_4 = lean_alloc_ctor(2, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -13332,9 +13501,11 @@ return x_4; static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__12() { _start: { -lean_object* x_1; -x_1 = lean_mk_string_from_bytes("@", 1); -return x_1; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticHave____1___closed__7; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; } } static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__13() { @@ -13342,7 +13513,7 @@ _start: { lean_object* x_1; lean_object* x_2; x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__12; -x_2 = lean_alloc_ctor(5, 1, 0); +x_2 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_2, 0, x_1); return x_2; } @@ -13351,21 +13522,29 @@ static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__14() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_rotateLeft___closed__6; -x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__13; -x_3 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_3, 0, x_1); -lean_ctor_set(x_3, 1, x_2); +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticHave____1___closed__4; +x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__15() { _start: { +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__14; +x_2 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__16() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__10; -x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__14; -x_3 = l_Lean_Parser_Tactic_intros___closed__9; +x_1 = l_Lean_Parser_Tactic_intros___closed__6; +x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__15; +x_3 = l_Lean_Parser_Tactic_case___closed__11; x_4 = lean_alloc_ctor(2, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -13373,25 +13552,13 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__16() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_first___closed__8; -x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__15; -x_3 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_3, 0, x_1); -lean_ctor_set(x_3, 1, x_2); -return x_3; -} -} static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__17() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Tactic_intros___closed__6; -x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__16; -x_3 = l_Lean_Parser_Tactic_intros___closed__11; +x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__13; +x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__16; x_4 = lean_alloc_ctor(2, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -13417,119 +13584,9 @@ static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__19() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__10; -x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__18; -x_3 = l_Lean_Parser_Tactic_tacticNext_______x3d_x3e_____closed__5; -x_4 = lean_alloc_ctor(2, 3, 0); -lean_ctor_set(x_4, 0, x_1); -lean_ctor_set(x_4, 1, x_2); -lean_ctor_set(x_4, 2, x_3); -return x_4; -} -} -static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__20() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__10; -x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__19; -x_3 = l_Lean_Parser_Tactic_rename___closed__8; -x_4 = lean_alloc_ctor(2, 3, 0); -lean_ctor_set(x_4, 0, x_1); -lean_ctor_set(x_4, 1, x_2); -lean_ctor_set(x_4, 2, x_3); -return x_4; -} -} -static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__21() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticHave____1___closed__7; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__22() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__21; -x_2 = lean_alloc_ctor(0, 1, 0); -lean_ctor_set(x_2, 0, x_1); -return x_2; -} -} -static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__23() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticHave____1___closed__4; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__24() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__23; -x_2 = lean_alloc_ctor(0, 1, 0); -lean_ctor_set(x_2, 0, x_1); -return x_2; -} -} -static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__25() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Tactic_intros___closed__6; -x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__24; -x_3 = l_Lean_Parser_Tactic_case___closed__11; -x_4 = lean_alloc_ctor(2, 3, 0); -lean_ctor_set(x_4, 0, x_1); -lean_ctor_set(x_4, 1, x_2); -lean_ctor_set(x_4, 2, x_3); -return x_4; -} -} -static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__26() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Tactic_intros___closed__6; -x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__22; -x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__25; -x_4 = lean_alloc_ctor(2, 3, 0); -lean_ctor_set(x_4, 0, x_1); -lean_ctor_set(x_4, 1, x_2); -lean_ctor_set(x_4, 2, x_3); -return x_4; -} -} -static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__27() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Tactic_withAnnotateState___closed__10; -x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__20; -x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__26; -x_4 = lean_alloc_ctor(2, 3, 0); -lean_ctor_set(x_4, 0, x_1); -lean_ctor_set(x_4, 1, x_2); -lean_ctor_set(x_4, 2, x_3); -return x_4; -} -} -static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt___closed__28() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__1; x_2 = l_Lean_Parser_Tactic_inductionAlt___closed__2; -x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__27; +x_3 = l_Lean_Parser_Tactic_inductionAlt___closed__18; x_4 = lean_alloc_ctor(9, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -13541,7 +13598,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_inductionAlt() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__28; +x_1 = l_Lean_Parser_Tactic_inductionAlt___closed__19; return x_1; } } @@ -19367,6 +19424,34 @@ l_Lean_Parser_Tactic_tacticLet_x27_____closed__6 = _init_l_Lean_Parser_Tactic_ta lean_mark_persistent(l_Lean_Parser_Tactic_tacticLet_x27_____closed__6); l_Lean_Parser_Tactic_tacticLet_x27__ = _init_l_Lean_Parser_Tactic_tacticLet_x27__(); lean_mark_persistent(l_Lean_Parser_Tactic_tacticLet_x27__); +l_Lean_Parser_Tactic_inductionAltLHS___closed__1 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__1); +l_Lean_Parser_Tactic_inductionAltLHS___closed__2 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__2); +l_Lean_Parser_Tactic_inductionAltLHS___closed__3 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__3); +l_Lean_Parser_Tactic_inductionAltLHS___closed__4 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__4); +l_Lean_Parser_Tactic_inductionAltLHS___closed__5 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__5(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__5); +l_Lean_Parser_Tactic_inductionAltLHS___closed__6 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__6(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__6); +l_Lean_Parser_Tactic_inductionAltLHS___closed__7 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__7(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__7); +l_Lean_Parser_Tactic_inductionAltLHS___closed__8 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__8(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__8); +l_Lean_Parser_Tactic_inductionAltLHS___closed__9 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__9(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__9); +l_Lean_Parser_Tactic_inductionAltLHS___closed__10 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__10(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__10); +l_Lean_Parser_Tactic_inductionAltLHS___closed__11 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__11(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__11); +l_Lean_Parser_Tactic_inductionAltLHS___closed__12 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__12(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__12); +l_Lean_Parser_Tactic_inductionAltLHS___closed__13 = _init_l_Lean_Parser_Tactic_inductionAltLHS___closed__13(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS___closed__13); +l_Lean_Parser_Tactic_inductionAltLHS = _init_l_Lean_Parser_Tactic_inductionAltLHS(); +lean_mark_persistent(l_Lean_Parser_Tactic_inductionAltLHS); l_Lean_Parser_Tactic_inductionAlt___closed__1 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__1); l_Lean_Parser_Tactic_inductionAlt___closed__2 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__2(); @@ -19405,24 +19490,6 @@ l_Lean_Parser_Tactic_inductionAlt___closed__18 = _init_l_Lean_Parser_Tactic_indu lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__18); l_Lean_Parser_Tactic_inductionAlt___closed__19 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__19(); lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__19); -l_Lean_Parser_Tactic_inductionAlt___closed__20 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__20(); -lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__20); -l_Lean_Parser_Tactic_inductionAlt___closed__21 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__21(); -lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__21); -l_Lean_Parser_Tactic_inductionAlt___closed__22 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__22(); -lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__22); -l_Lean_Parser_Tactic_inductionAlt___closed__23 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__23(); -lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__23); -l_Lean_Parser_Tactic_inductionAlt___closed__24 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__24(); -lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__24); -l_Lean_Parser_Tactic_inductionAlt___closed__25 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__25(); -lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__25); -l_Lean_Parser_Tactic_inductionAlt___closed__26 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__26(); -lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__26); -l_Lean_Parser_Tactic_inductionAlt___closed__27 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__27(); -lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__27); -l_Lean_Parser_Tactic_inductionAlt___closed__28 = _init_l_Lean_Parser_Tactic_inductionAlt___closed__28(); -lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt___closed__28); l_Lean_Parser_Tactic_inductionAlt = _init_l_Lean_Parser_Tactic_inductionAlt(); lean_mark_persistent(l_Lean_Parser_Tactic_inductionAlt); l_Lean_Parser_Tactic_inductionAlts___closed__1 = _init_l_Lean_Parser_Tactic_inductionAlts___closed__1(); diff --git a/stage0/stdlib/Lean/Elab/Tactic/Induction.c b/stage0/stdlib/Lean/Elab/Tactic/Induction.c index 2035ab388d..8489c37441 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/Induction.c +++ b/stage0/stdlib/Lean/Elab/Tactic/Induction.c @@ -16,6 +16,7 @@ extern "C" { LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_ElimApp_mkElimApp_loop___spec__1___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_Lean_Elab_Tactic_ElimApp_mkElimApp_loop___closed__3; static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_go___lambda__2___closed__1; +static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7101____closed__1; static lean_object* l_Lean_Elab_Tactic_isHoleRHS___closed__6; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCases(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_evalInduction_checkTargets___spec__1___closed__2; @@ -39,7 +40,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tacti lean_object* lean_erase_macro_scopes(lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_evalInduction___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_evalInduction_checkTargets___spec__1___closed__1; -LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7143_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7101_(lean_object*); lean_object* l_Lean_stringToMessageData(lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_evalInduction_checkTargets___spec__1___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_evalCases_declRange___closed__6; @@ -196,7 +197,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___lambda__2___boxed(le LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__3___closed__1; LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInduction(lean_object*); -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isNewAlt___boxed(lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltRHS___boxed(lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec__5___lambda__2___boxed(lean_object**); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getArgExpectedType___boxed(lean_object*); @@ -223,7 +223,6 @@ lean_object* lean_st_ref_take(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstNoOverload___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___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_evalCases___closed__5; static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec__5___lambda__2___closed__4; -static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7143____closed__1; static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange___closed__3; lean_object* lean_nat_sub(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -373,7 +372,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tac LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___lambda__3___boxed(lean_object**); lean_object* l_Lean_Elab_Term_mkConst(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_reorderAlts___lambda__1___boxed(lean_object*, lean_object*, lean_object*); -LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isNewAlt(lean_object*); lean_object* l_Lean_Elab_Tactic_elabTermEnsuringType(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_isHoleRHS___closed__3; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getFType___boxed(lean_object*); @@ -602,50 +600,18 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts___boxed(lean_object LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___spec__1(lean_object*, uint8_t, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(lean_object*); uint8_t l_Lean_Syntax_isIdent(lean_object*); -LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isNewAlt(lean_object* x_1) { -_start: -{ -lean_object* x_2; lean_object* x_3; uint8_t x_4; -x_2 = l_Lean_Syntax_getNumArgs(x_1); -x_3 = lean_unsigned_to_nat(3u); -x_4 = lean_nat_dec_eq(x_2, x_3); -lean_dec(x_2); -return x_4; -} -} -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isNewAlt___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_isNewAlt(x_1); -lean_dec(x_1); -x_3 = lean_box(x_2); -return x_3; -} -} LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(lean_object* x_1) { _start: { -uint8_t x_2; -x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isNewAlt(x_1); -if (x_2 == 0) -{ -uint8_t x_3; -x_3 = 0; -return x_3; -} -else -{ -lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; -x_4 = lean_unsigned_to_nat(0u); -x_5 = l_Lean_Syntax_getArg(x_1, x_4); -x_6 = l_Lean_Syntax_getNumArgs(x_5); -lean_dec(x_5); -x_7 = lean_unsigned_to_nat(1u); -x_8 = lean_nat_dec_lt(x_7, x_6); -lean_dec(x_6); -return x_8; -} +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; +x_2 = lean_unsigned_to_nat(0u); +x_3 = l_Lean_Syntax_getArg(x_1, x_2); +x_4 = l_Lean_Syntax_getNumArgs(x_3); +lean_dec(x_3); +x_5 = lean_unsigned_to_nat(1u); +x_6 = lean_nat_dec_lt(x_5, x_4); +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) { @@ -747,22 +713,12 @@ return x_7; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getFirstAltLhs(lean_object* x_1) { _start: { -uint8_t x_2; -x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isNewAlt(x_1); -if (x_2 == 0) -{ -lean_inc(x_1); -return x_1; -} -else -{ -lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_3 = lean_unsigned_to_nat(0u); -x_4 = l_Lean_Syntax_getArg(x_1, x_3); -x_5 = l_Lean_Syntax_getArg(x_4, x_3); -lean_dec(x_4); -return x_5; -} +lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_2 = lean_unsigned_to_nat(0u); +x_3 = l_Lean_Syntax_getArg(x_1, x_2); +x_4 = l_Lean_Syntax_getArg(x_3, x_2); +lean_dec(x_3); +return x_4; } } LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getFirstAltLhs___boxed(lean_object* x_1) { @@ -955,22 +911,10 @@ return x_6; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltRHS(lean_object* x_1) { _start: { -uint8_t x_2; -x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isNewAlt(x_1); -if (x_2 == 0) -{ -lean_object* x_3; lean_object* x_4; -x_3 = lean_unsigned_to_nat(4u); -x_4 = l_Lean_Syntax_getArg(x_1, x_3); -return x_4; -} -else -{ -lean_object* x_5; lean_object* x_6; -x_5 = lean_unsigned_to_nat(2u); -x_6 = l_Lean_Syntax_getArg(x_1, x_5); -return x_6; -} +lean_object* x_2; lean_object* x_3; +x_2 = lean_unsigned_to_nat(2u); +x_3 = l_Lean_Syntax_getArg(x_1, x_2); +return x_3; } } LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltRHS___boxed(lean_object* x_1) { @@ -985,22 +929,10 @@ return x_2; LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltDArrow(lean_object* x_1) { _start: { -uint8_t x_2; -x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isNewAlt(x_1); -if (x_2 == 0) -{ -lean_object* x_3; lean_object* x_4; -x_3 = lean_unsigned_to_nat(3u); -x_4 = l_Lean_Syntax_getArg(x_1, x_3); -return x_4; -} -else -{ -lean_object* x_5; lean_object* x_6; -x_5 = lean_unsigned_to_nat(1u); -x_6 = l_Lean_Syntax_getArg(x_1, x_5); -return x_6; -} +lean_object* x_2; lean_object* x_3; +x_2 = lean_unsigned_to_nat(1u); +x_3 = l_Lean_Syntax_getArg(x_1, x_2); +return x_3; } } LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltDArrow___boxed(lean_object* x_1) { @@ -1693,42 +1625,44 @@ return x_24; 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; uint8_t x_15; -x_13 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltRHS(x_2); -x_14 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltDArrow(x_2); -lean_inc(x_13); -x_15 = l_Lean_Elab_Tactic_isHoleRHS(x_13); -if (x_15 == 0) +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) { -lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; -x_16 = lean_box(0); -x_17 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_17, 0, x_1); -lean_ctor_set(x_17, 1, x_16); -lean_inc(x_13); -x_18 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__1), 13, 4); -lean_closure_set(x_18, 0, x_17); -lean_closure_set(x_18, 1, x_13); -lean_closure_set(x_18, 2, x_2); -lean_closure_set(x_18, 3, x_3); -x_19 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1(x_14, x_13, 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_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; +x_18 = lean_box(0); +x_19 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_19, 0, x_1); +lean_ctor_set(x_19, 1, x_18); +lean_inc(x_14); +x_20 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__1), 13, 4); +lean_closure_set(x_20, 0, x_19); +lean_closure_set(x_20, 1, x_14); +lean_closure_set(x_20, 2, x_2); +lean_closure_set(x_20, 3, x_3); +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; } else { -lean_object* x_20; lean_object* x_21; lean_object* x_22; +lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_dec(x_2); lean_inc(x_1); -lean_inc(x_13); -x_20 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__2___boxed), 11, 2); -lean_closure_set(x_20, 0, x_13); -lean_closure_set(x_20, 1, x_1); -x_21 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__3), 12, 3); -lean_closure_set(x_21, 0, x_1); -lean_closure_set(x_21, 1, x_20); -lean_closure_set(x_21, 2, x_3); -x_22 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1(x_14, x_13, x_21, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); -return x_22; +lean_inc(x_14); +x_22 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__2___boxed), 11, 2); +lean_closure_set(x_22, 0, x_14); +lean_closure_set(x_22, 1, x_1); +x_23 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalAlt___lambda__3), 12, 3); +lean_closure_set(x_23, 0, x_1); +lean_closure_set(x_23, 1, x_22); +lean_closure_set(x_23, 2, x_3); +x_24 = l_Lean_Elab_Tactic_withCaseRef___at_Lean_Elab_Tactic_evalAlt___spec__1(x_16, x_14, x_23, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); +return x_24; } } } @@ -18441,7 +18375,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalInduction_declRang _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(457u); +x_1 = lean_unsigned_to_nat(445u); x_2 = lean_unsigned_to_nat(46u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -18453,7 +18387,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalInduction_declRang _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(489u); +x_1 = lean_unsigned_to_nat(477u); x_2 = lean_unsigned_to_nat(92u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -18481,7 +18415,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalInduction_declRang _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(457u); +x_1 = lean_unsigned_to_nat(445u); x_2 = lean_unsigned_to_nat(50u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -18493,7 +18427,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalInduction_declRang _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(457u); +x_1 = lean_unsigned_to_nat(445u); x_2 = lean_unsigned_to_nat(63u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -20689,7 +20623,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange___ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(513u); +x_1 = lean_unsigned_to_nat(501u); x_2 = lean_unsigned_to_nat(42u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -20701,7 +20635,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange___ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(536u); +x_1 = lean_unsigned_to_nat(524u); x_2 = lean_unsigned_to_nat(116u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -20729,7 +20663,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange___ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(513u); +x_1 = lean_unsigned_to_nat(501u); x_2 = lean_unsigned_to_nat(46u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -20741,7 +20675,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange___ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_unsigned_to_nat(513u); +x_1 = lean_unsigned_to_nat(501u); x_2 = lean_unsigned_to_nat(55u); x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); @@ -20787,7 +20721,7 @@ x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1); return x_4; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7143____closed__1() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7101____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -20797,11 +20731,11 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7143_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7101_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7143____closed__1; +x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7101____closed__1; x_3 = l_Lean_registerTraceClass(x_2, x_1); if (lean_obj_tag(x_3) == 0) { @@ -21184,9 +21118,9 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange___close res = l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange(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_7143____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7143____closed__1(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7143____closed__1); -res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7143_(lean_io_mk_world()); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7101____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7101____closed__1(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7101____closed__1); +res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7101_(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));