chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
daeb271678
commit
2dad133208
5 changed files with 1159 additions and 1077 deletions
3
stage0/src/Init/Tactics.lean
generated
3
stage0/src/Init/Tactics.lean
generated
|
|
@ -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,
|
||||
|
|
|
|||
32
stage0/src/Lean/Elab/Tactic/Induction.lean
generated
32
stage0/src/Lean/Elab/Tactic/Induction.lean
generated
|
|
@ -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 :=
|
||||
|
|
|
|||
1576
stage0/stdlib/Init/Classical.c
generated
1576
stage0/stdlib/Init/Classical.c
generated
File diff suppressed because it is too large
Load diff
417
stage0/stdlib/Init/Tactics.c
generated
417
stage0/stdlib/Init/Tactics.c
generated
|
|
@ -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();
|
||||
|
|
|
|||
208
stage0/stdlib/Lean/Elab/Tactic/Induction.c
generated
208
stage0/stdlib/Lean/Elab/Tactic/Induction.c
generated
|
|
@ -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));
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue