max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-14 16:23:49 -07:00
parent 05778565ab
commit 5193c6d0ef
10 changed files with 3438 additions and 1601 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
stage0/src/Init/Conv.lean generated
View file

@ -26,7 +26,7 @@ syntax (name := whnf) "whnf" : conv
/-- Put term in normal form, this tactic is ment for debugging purposes only -/
syntax (name := reduce) "reduce" : conv
syntax (name := congr) "congr" : conv
syntax (name := arg) "arg " num : conv
syntax (name := arg) "arg " "@"? num : conv
syntax (name := ext) "ext " (colGt ident)* : conv
syntax (name := change) "change " term : conv
syntax (name := delta) "delta " ident : conv
@ -54,10 +54,11 @@ macro "left" : conv => `(lhs)
macro "right" : conv => `(rhs)
macro "intro " xs:(colGt ident)* : conv => `(ext $xs*)
syntax enterArg := ident <|> num
syntax enterArg := ident <|> group("@"? num)
syntax "enter " "[" (colGt enterArg),+ "]": conv
macro_rules
| `(conv| enter [$i:num]) => `(conv| arg $i)
| `(conv| enter [@$i:num]) => `(conv| arg @$i)
| `(conv| enter [$id:ident]) => `(conv| ext $id)
| `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))

20
stage0/src/Lean/Elab/Tactic/Conv/Congr.lean generated
View file

@ -11,7 +11,8 @@ open Meta
/-- Returns a list of new congruence subgoals, which contains `none` for each argument with
forward dependencies. -/
private def congrApp (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List (Option MVarId)) :=
private def congrApp (mvarId : MVarId) (lhs rhs : Expr) (addImplicitArgs := false) :
MetaM (List (Option MVarId)) :=
-- TODO: add support for `[congr]` lemmas
lhs.withApp fun f args => do
let infos := (← getFunInfoNArgs f args.size).paramInfo
@ -19,10 +20,11 @@ private def congrApp (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List (Option MV
let mut newGoals : Array (Option MVarId) := #[]
let mut i := 0
for arg in args do
let addGoal ← if i < infos.size then
pure infos[i].binderInfo.isExplicit
else
pure (← whnfD (← inferType r.expr)).isArrow
let addGoal ←
if i < infos.size then
pure (addImplicitArgs || infos[i].binderInfo.isExplicit)
else
pure (← whnfD (← inferType r.expr)).isArrow
let hasFwdDep := i < infos.size && infos[i].hasFwdDeps
if addGoal then
if hasFwdDep then
@ -54,14 +56,14 @@ def isImplies (e : Expr) : MetaM Bool :=
else
return false
def congr (mvarId : MVarId) : MetaM (List (Option MVarId)) :=
def congr (mvarId : MVarId) (addImplicitArgs := false) : MetaM (List (Option MVarId)) :=
withMVarContext mvarId do
let (lhs, rhs) ← getLhsRhsCore mvarId
let lhs := (← instantiateMVars lhs).consumeMData
if (← isImplies lhs) then
return (← congrImplies mvarId).map Option.some
else if lhs.isApp then
congrApp mvarId lhs rhs
congrApp mvarId lhs rhs addImplicitArgs
else
throwError "invalid 'congr' conv tactic, application or implication expected{indentExpr lhs}"
@ -95,12 +97,12 @@ private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i
@[builtinTactic Lean.Parser.Tactic.Conv.arg] def evalArg : Tactic := fun stx => do
match stx with
| `(conv| arg $i) =>
| `(conv| arg $[@%$tk?]? $i:num) =>
let i := i.isNatLit?.getD 0
if i == 0 then
throwError "invalid 'arg' conv tactic, index must be greater than 0"
let i := i - 1
let mvarIds ← congr (← getMainGoal)
let mvarIds ← congr (← getMainGoal) (addImplicitArgs := tk?.isSome)
selectIdx "arg" mvarIds i
| _ => throwUnsupportedSyntax

177
stage0/src/Lean/Elab/Tactic/Induction.lean generated
View file

@ -25,18 +25,8 @@ open Meta
syntax inductionAlt := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq)
```
-/
private def isMultiAlt (alt : Syntax) : Bool :=
alt[0].getNumArgs > 1
private def expandMultiAlt? (alt : Syntax) : Option (Array Syntax) := Id.run do
if isMultiAlt alt then
some <| alt[0].getArgs.map fun lhs => alt.setArg 0 (mkNullNode #[lhs])
else
none
private def getFirstAltLhs (alt : Syntax) : Syntax :=
alt[0][0]
/-- Return `inductionAlt` name. It assumes `alt` does not have multiple `inductionAltLHS` -/
private def getAltName (alt : Syntax) : Name :=
let lhs := getFirstAltLhs alt
@ -376,7 +366,13 @@ private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Exp
let (fvarIds, mvarId') ← Meta.revert mvarId fvarIds
return (fvarIds.size, mvarId')
-- syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
/--
Given `inductionAlts` of the fom
```
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
```
Return an array containing its alternatives.
-/
private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
inductionAlts[2].getArgs
@ -386,6 +382,65 @@ private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax
private def getOptPreTacOfOptInductionAlts (optInductionAlts : Syntax) : Syntax :=
if optInductionAlts.isNone then mkNullNode else optInductionAlts[0][1]
private def isMultiAlt (alt : Syntax) : Bool :=
alt[0].getNumArgs > 1
/-- Return `some #[alt_1, ..., alt_n]` if `alt` has multiple LHSs. -/
private def expandMultiAlt? (alt : Syntax) : Option (Array Syntax) := Id.run do
if isMultiAlt alt then
some <| alt[0].getArgs.map fun lhs => alt.setArg 0 (mkNullNode #[lhs])
else
none
/--
Given `inductionAlts` of the form
```
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
```
Return `some inductionAlts'` if one of the alternatives have multiple LHSs, in the new `inductionAlts'`
all alternatives have a single LHS.
Remark: the `RHS` of alternatives with multi LHSs is copied.
-/
private def expandInductionAlts? (inductionAlts : Syntax) : Option Syntax := Id.run do
let alts := getAltsOfInductionAlts inductionAlts
if alts.any isMultiAlt then
let mut altsNew := #[]
for alt in alts do
if let some alt' := expandMultiAlt? alt then
altsNew := altsNew ++ alt'
else
altsNew := altsNew.push alt
some <| inductionAlts.setArg 2 (mkNullNode altsNew)
else
none
/--
Expand
```
syntax "induction " term,+ (" using " ident)? ("generalizing " (colGt term:max)+)? (inductionAlts)? : tactic
```
if `inductionAlts` has an alternative with multiple LHSs.
-/
private def expandInduction? (induction : Syntax) : Option Syntax := do
let optInductionAlts := induction[4]
guard <| !optInductionAlts.isNone
let inductionAlts' ← expandInductionAlts? optInductionAlts[0]
return induction.setArg 4 (mkNullNode #[inductionAlts'])
/--
Expand
```
syntax "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
```
if `inductionAlts` has an alternative with multiple LHSs.
-/
private def expandCases? (induction : Syntax) : Option Syntax := do
let optInductionAlts := induction[3]
guard <| !optInductionAlts.isNone
let inductionAlts' ← expandInductionAlts? optInductionAlts[0]
return induction.setArg 3 (mkNullNode #[inductionAlts'])
/-
We may have at most one `| _ => ...` (wildcard alternative), and it must not set variable names.
The idea is to make sure users do not write unstructured tactics. -/
@ -442,31 +497,34 @@ private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
else
return exprs
@[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx => focus do
let optInductionAlts := stx[4]
let alts := getAltsOfOptInductionAlts optInductionAlts
let targets ← withMainContext <| stx[1].getSepArgs.mapM (elabTerm · none)
let targets ← generalizeTargets targets
let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := true)
let mvarId ← getMainGoal
-- save initial info before main goal is reassigned
let initInfo ← mkTacticInfo (← getMCtx) (← getUnsolvedGoals) (← getRef)
let tag ← getMVarTag mvarId
withMVarContext mvarId do
let targets ← addImplicitTargets elimInfo targets
checkTargets targets
let targetFVarIds := targets.map (·.fvarId!)
let (n, mvarId) ← generalizeVars mvarId stx targets
@[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx =>
match expandInduction? stx with
| some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
| _ => focus do
let optInductionAlts := stx[4]
let alts := getAltsOfOptInductionAlts optInductionAlts
let targets ← withMainContext <| stx[1].getSepArgs.mapM (elabTerm · none)
let targets ← generalizeTargets targets
let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := true)
let mvarId ← getMainGoal
-- save initial info before main goal is reassigned
let initInfo ← mkTacticInfo (← getMCtx) (← getUnsolvedGoals) (← getRef)
let tag ← getMVarTag mvarId
withMVarContext mvarId do
let result ← withRef stx[1] do -- use target position as reference
ElimApp.mkElimApp elimInfo targets tag
trace[Elab.induction] "elimApp: {result.elimApp}"
let elimArgs := result.elimApp.getAppArgs
ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetFVarIds
let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
assignExprMVar mvarId result.elimApp
ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numGeneralized := n) (toClear := targetFVarIds)
appendGoals result.others.toList
let targets ← addImplicitTargets elimInfo targets
checkTargets targets
let targetFVarIds := targets.map (·.fvarId!)
let (n, mvarId) ← generalizeVars mvarId stx targets
withMVarContext mvarId do
let result ← withRef stx[1] do -- use target position as reference
ElimApp.mkElimApp elimInfo targets tag
trace[Elab.induction] "elimApp: {result.elimApp}"
let elimArgs := result.elimApp.getAppArgs
ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetFVarIds
let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
assignExprMVar mvarId result.elimApp
ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numGeneralized := n) (toClear := targetFVarIds)
appendGoals result.others.toList
where
checkTargets (targets : Array Expr) : MetaM Unit := do
let mut foundFVars : FVarIdSet := {}
@ -498,30 +556,33 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) :=
else
return args.map (·.expr)
@[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx => focus do
-- leading_parser nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> optInductionAlts
let targets ← elabCasesTargets stx[1].getSepArgs
let optInductionAlts := stx[3]
let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
let alts := getAltsOfOptInductionAlts optInductionAlts
let targetRef := stx[1]
let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := false)
let mvarId ← getMainGoal
-- save initial info before main goal is reassigned
let initInfo ← mkTacticInfo (← getMCtx) (← getUnsolvedGoals) (← getRef)
let tag ← getMVarTag mvarId
withMVarContext mvarId do
let targets ← addImplicitTargets elimInfo targets
let result ← withRef targetRef <| ElimApp.mkElimApp elimInfo targets tag
let elimArgs := result.elimApp.getAppArgs
let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i]
let motiveType ← inferType elimArgs[elimInfo.motivePos]
let mvarId ← generalizeTargetsEq mvarId motiveType targets
let (targetsNew, mvarId) ← introN mvarId targets.size
@[builtinTactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx =>
match expandCases? stx with
| some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
| _ => focus do
-- leading_parser nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> optInductionAlts
let targets ← elabCasesTargets stx[1].getSepArgs
let optInductionAlts := stx[3]
let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
let alts := getAltsOfOptInductionAlts optInductionAlts
let targetRef := stx[1]
let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := false)
let mvarId ← getMainGoal
-- save initial info before main goal is reassigned
let initInfo ← mkTacticInfo (← getMCtx) (← getUnsolvedGoals) (← getRef)
let tag ← getMVarTag mvarId
withMVarContext mvarId do
ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetsNew
assignExprMVar mvarId result.elimApp
ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numEqs := targets.size) (toClear := targetsNew)
let targets ← addImplicitTargets elimInfo targets
let result ← withRef targetRef <| ElimApp.mkElimApp elimInfo targets tag
let elimArgs := result.elimApp.getAppArgs
let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i]
let motiveType ← inferType elimArgs[elimInfo.motivePos]
let mvarId ← generalizeTargetsEq mvarId motiveType targets
let (targetsNew, mvarId) ← introN mvarId targets.size
withMVarContext mvarId do
ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos].mvarId! targetsNew
assignExprMVar mvarId result.elimApp
ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numEqs := targets.size) (toClear := targetsNew)
builtin_initialize
registerTraceClass `Elab.cases

52
stage0/src/Lean/Linter/Basic.lean generated
View file

@ -124,7 +124,7 @@ def unusedVariables : Linter := fun stx => do
return ()
where
skipDeclIdIfPresent (stx : Syntax) : Syntax :=
if stx.isOfKind `Lean.Parser.Command.declId then
if stx.isOfKind ``Lean.Parser.Command.declId then
stx[0]
else
stx
@ -133,69 +133,69 @@ where
let some declRange := stx.getRange?
| false
constDecls.contains declRange &&
!stackMatches stack [`Lean.Parser.Term.letIdDecl]
!stackMatches stack [``Lean.Parser.Term.letIdDecl]
matchesUnusedPattern (stx : Syntax) (_ : SyntaxStack) :=
stx.getId.toString.startsWith "_"
isVariable (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, none, `null, `Lean.Parser.Command.variable]
stackMatches stack [`null, none, `null, ``Lean.Parser.Command.variable]
isInStructure (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, none, `null, `Lean.Parser.Command.structure]
stackMatches stack [`null, none, `null, ``Lean.Parser.Command.structure]
isInInductive (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, none, `null, none, `Lean.Parser.Command.inductive] &&
stackMatches stack [`null, none, `null, none, ``Lean.Parser.Command.inductive] &&
(stack.get? 3 |>.any fun (stx, pos) =>
pos == 0 &&
[`Lean.Parser.Command.optDeclSig, `Lean.Parser.Command.declSig].any (stx.isOfKind ·))
[``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·))
isInCtorOrStructBinder (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, none, `null, `Lean.Parser.Command.optDeclSig, none] &&
stackMatches stack [`null, none, `null, ``Lean.Parser.Command.optDeclSig, none] &&
(stack.get? 4 |>.any fun (stx, _) =>
[`Lean.Parser.Command.ctor, `Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·))
[``Lean.Parser.Command.ctor, ``Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·))
isInConstantOrAxiom (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, none, `null, `Lean.Parser.Command.declSig, none] &&
stackMatches stack [`null, none, `null, ``Lean.Parser.Command.declSig, none] &&
(stack.get? 4 |>.any fun (stx, _) =>
[`Lean.Parser.Command.constant, `Lean.Parser.Command.axiom].any (stx.isOfKind ·))
[``Lean.Parser.Command.constant, ``Lean.Parser.Command.axiom].any (stx.isOfKind ·))
isInDefWithForeignDefinition (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, none, `null, none, none, `Lean.Parser.Command.declaration] &&
stackMatches stack [`null, none, `null, none, none, ``Lean.Parser.Command.declaration] &&
(stack.get? 3 |>.any fun (stx, _) =>
stx.isOfKind `Lean.Parser.Command.optDeclSig ||
stx.isOfKind `Lean.Parser.Command.declSig) &&
stx.isOfKind ``Lean.Parser.Command.optDeclSig ||
stx.isOfKind ``Lean.Parser.Command.declSig) &&
(stack.get? 5 |>.any fun (stx, _) => Id.run <| do
let declModifiers := stx[0]
if !declModifiers.isOfKind `Lean.Parser.Command.declModifiers then
if !declModifiers.isOfKind ``Lean.Parser.Command.declModifiers then
return false
let termAttributes := declModifiers[1][0]
if !termAttributes.isOfKind `Lean.Parser.Term.attributes then
if !termAttributes.isOfKind ``Lean.Parser.Term.attributes then
return false
let termAttrInstance := termAttributes[1][0]
if !termAttrInstance.isOfKind `Lean.Parser.Term.attrInstance then
if !termAttrInstance.isOfKind ``Lean.Parser.Term.attrInstance then
return false
let attr := termAttrInstance[1]
if attr.isOfKind `Lean.Parser.Attr.extern then
if attr.isOfKind ``Lean.Parser.Attr.extern then
return true
else if attr.isOfKind `Lean.Parser.Attr.simple then
else if attr.isOfKind ``Lean.Parser.Attr.simple then
return attr[0].getId == `implementedBy
else
return false)
isInDepArrow (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, `Lean.Parser.Term.explicitBinder, `Lean.Parser.Term.depArrow]
stackMatches stack [`null, ``Lean.Parser.Term.explicitBinder, ``Lean.Parser.Term.depArrow]
isInLetDeclaration (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, none, `null, `Lean.Parser.Term.letIdDecl, none] &&
stackMatches stack [`null, none, `null, ``Lean.Parser.Term.letIdDecl, none] &&
(stack.get? 3 |>.any fun (_, pos) => pos == 1) &&
(stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind `Lean.Parser.Command.whereStructField)
(stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind ``Lean.Parser.Command.whereStructField)
isInDeclarationSignature (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, none, `null, none] &&
(stack.get? 3 |>.any fun (stx, pos) =>
pos == 0 &&
[`Lean.Parser.Command.optDeclSig, `Lean.Parser.Command.declSig].any (stx.isOfKind ·))
[``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·))
isInFun (_ : Syntax) (stack : SyntaxStack) :=
stackMatches stack [`null, `Lean.Parser.Term.basicFun] ||
stackMatches stack [`null, `Lean.Parser.Term.paren, `null, `Lean.Parser.Term.basicFun]
stackMatches stack [`null, ``Lean.Parser.Term.basicFun] ||
stackMatches stack [`null, ``Lean.Parser.Term.paren, `null, ``Lean.Parser.Term.basicFun]
isPatternVar (_ : Syntax) (stack : SyntaxStack) :=
stack.any fun (stx, pos) =>
(stx.isOfKind `Lean.Parser.Term.matchAlt && pos == 1) ||
(stx.isOfKind `Lean.Parser.Tactic.inductionAlt && pos == 2)
(stx.isOfKind ``Lean.Parser.Term.matchAlt && pos == 1) ||
(stx.isOfKind ``Lean.Parser.Tactic.inductionAltLHS && pos == 2)
builtin_initialize addLinter unusedVariables

3
stage0/src/Lean/Parser/Command.lean generated
View file

@ -71,6 +71,7 @@ def optDefDeriving := optional (atomic ("deriving " >> notSymbol "instance") >
def «def» := leading_parser "def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
def «theorem» := leading_parser "theorem " >> declId >> ppIndent declSig >> declVal >> terminationSuffix
def «constant» := leading_parser "constant " >> declId >> ppIndent declSig >> optional declValSimple
def «opaque» := leading_parser "opaque " >> declId >> ppIndent declSig >> optional declValSimple
/- As `declSig` starts with a space, "instance" does not need a trailing space if we put `ppSpace` in the optional fragments. -/
def «instance» := leading_parser Term.attrKind >> "instance" >> optNamedPrio >> optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix
def «axiom» := leading_parser "axiom " >> declId >> ppIndent declSig
@ -95,7 +96,7 @@ def «structure» := leading_parser
>> optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields)
>> optDeriving
@[builtinCommandParser] def declaration := leading_parser
declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
@[builtinCommandParser] def «deriving» := leading_parser "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 ident ", "
@[builtinCommandParser] def noncomputableSection := leading_parser "noncomputable " >> "section " >> optional ident
@[builtinCommandParser] def «section» := leading_parser "section " >> optional ident

350
stage0/stdlib/Init/Conv.c generated
View file

@ -101,6 +101,7 @@ static lean_object* l_Lean_Parser_Tactic_Conv_convEnter_x5b_____x5d___closed__5;
static lean_object* l_Lean_Parser_Tactic_Conv_change___closed__6;
lean_object* lean_array_push(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__convDone__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_Conv_arg___closed__11;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_Conv_convRepeat__;
static lean_object* l_Lean_Parser_Tactic_Conv_convRepeat_____closed__5;
static lean_object* l_Lean_Parser_Tactic_Conv_convArgs___closed__5;
@ -175,6 +176,7 @@ static lean_object* l_Lean_Parser_Tactic_Conv_rhs___closed__2;
static lean_object* l_Lean_Parser_Tactic_Conv_first___closed__2;
static lean_object* l_Lean_Parser_Tactic_Conv_conv_xb7_x2e_____closed__8;
static lean_object* l_Lean_Parser_Tactic_Conv_simp___closed__26;
static lean_object* l_Lean_Parser_Tactic_Conv_enterArg___closed__6;
static lean_object* l_Lean_Parser_Tactic_Conv_conv_quot___closed__6;
static lean_object* l_Lean_Parser_Tactic_Conv_first___closed__1;
static lean_object* l_Lean_Parser_Tactic_Conv_conv___closed__20;
@ -250,6 +252,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_Conv_ext;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__convArgs__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Tactic_Conv_convSeqBracketed___closed__11;
static lean_object* l_Lean_Parser_Tactic_Conv_convConvSeq___closed__2;
static lean_object* l_Lean_Parser_Tactic_Conv_arg___closed__12;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_Conv_convArgs;
static lean_object* l_Lean_Parser_Tactic_Conv_convErw_____closed__5;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_Conv_first;
@ -331,6 +334,7 @@ static lean_object* l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules_
static lean_object* l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__6;
static lean_object* l_Lean_Parser_Tactic_Conv_convErw_____closed__4;
static lean_object* l_Lean_Parser_Tactic_Conv_simp___closed__15;
static lean_object* l_Lean_Parser_Tactic_Conv_enterArg___closed__5;
static lean_object* l_Lean_Parser_Tactic_Conv_convErw_____closed__1;
static lean_object* l_Lean_Parser_Tactic_Conv_nestedTacticCore___closed__4;
static lean_object* l_Lean_Parser_Tactic_Conv_convRw_______closed__3;
@ -404,6 +408,7 @@ lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_Conv_pattern;
static lean_object* l_Lean_Parser_Tactic_Conv_convRw_______closed__2;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_Conv_convSeq1Indented;
static lean_object* l_Lean_Parser_Tactic_Conv_arg___closed__10;
static lean_object* l_Lean_Parser_Tactic_Conv_convSeq1Indented___closed__25;
static lean_object* l_Lean_Parser_Tactic_Conv_ext___closed__11;
static lean_object* l_Lean_Parser_Tactic_Conv_rhs___closed__4;
@ -468,6 +473,7 @@ static lean_object* l_Lean_Parser_Tactic_Conv_convEnter_x5b_____x5d___closed__9;
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_Conv_convDone;
static lean_object* l_Lean_Parser_Tactic_Conv_conv_quot___closed__15;
static lean_object* l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__convErw____1___closed__23;
static lean_object* l_Lean_Parser_Tactic_Conv_arg___closed__13;
static lean_object* l_Lean_Parser_Tactic_Conv_nestedConv___closed__2;
static lean_object* _init_l_Lean_Parser_Tactic_Conv_conv_quot___closed__1() {
_start:
@ -1733,28 +1739,30 @@ static lean_object* _init_l_Lean_Parser_Tactic_Conv_arg___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("num", 3);
x_1 = lean_mk_string_from_bytes("@", 1);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_Conv_arg___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Tactic_Conv_arg___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_Conv_arg___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_Conv_arg___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_Conv_arg___closed__6;
x_2 = lean_alloc_ctor(0, 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;
x_1 = l_Lean_Parser_Tactic_Conv_convSeq1Indented___closed__18;
x_2 = l_Lean_Parser_Tactic_Conv_arg___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_Conv_arg___closed__8() {
@ -1774,10 +1782,52 @@ return x_4;
static lean_object* _init_l_Lean_Parser_Tactic_Conv_arg___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("num", 3);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_Conv_arg___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Tactic_Conv_arg___closed__9;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_Tactic_Conv_arg___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_Conv_arg___closed__10;
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_Conv_arg___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_Conv_conv_quot___closed__10;
x_2 = l_Lean_Parser_Tactic_Conv_arg___closed__8;
x_3 = l_Lean_Parser_Tactic_Conv_arg___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_Conv_arg___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_Conv_arg___closed__2;
x_2 = lean_unsigned_to_nat(1022u);
x_3 = l_Lean_Parser_Tactic_Conv_arg___closed__8;
x_3 = l_Lean_Parser_Tactic_Conv_arg___closed__12;
x_4 = lean_alloc_ctor(3, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -1789,7 +1839,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_Conv_arg() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_Conv_arg___closed__9;
x_1 = l_Lean_Parser_Tactic_Conv_arg___closed__13;
return x_1;
}
}
@ -5055,9 +5105,9 @@ static lean_object* _init_l_Lean_Parser_Tactic_Conv_enterArg___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_Conv_convSeq___closed__4;
x_2 = l_Lean_Parser_Tactic_Conv_conv___closed__8;
x_3 = l_Lean_Parser_Tactic_Conv_arg___closed__7;
x_1 = l_Lean_Parser_Tactic_Conv_conv_quot___closed__10;
x_2 = l_Lean_Parser_Tactic_Conv_arg___closed__7;
x_3 = l_Lean_Parser_Tactic_Conv_arg___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);
@ -5068,10 +5118,36 @@ return x_4;
static lean_object* _init_l_Lean_Parser_Tactic_Conv_enterArg___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_Conv_convSeq1Indented___closed__12;
x_2 = l_Lean_Parser_Tactic_Conv_enterArg___closed__3;
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_Conv_enterArg___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_Conv_convSeq___closed__4;
x_2 = l_Lean_Parser_Tactic_Conv_conv___closed__8;
x_3 = l_Lean_Parser_Tactic_Conv_enterArg___closed__4;
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_Conv_enterArg___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_Conv_enterArg___closed__1;
x_2 = l_Lean_Parser_Tactic_Conv_enterArg___closed__2;
x_3 = l_Lean_Parser_Tactic_Conv_enterArg___closed__3;
x_3 = l_Lean_Parser_Tactic_Conv_enterArg___closed__5;
x_4 = lean_alloc_ctor(9, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -5083,7 +5159,7 @@ static lean_object* _init_l_Lean_Parser_Tactic_Conv_enterArg() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_Conv_enterArg___closed__4;
x_1 = l_Lean_Parser_Tactic_Conv_enterArg___closed__6;
return x_1;
}
}
@ -5579,7 +5655,7 @@ else
lean_object* x_149; lean_object* x_150; uint8_t x_151;
x_149 = l_Lean_Syntax_getArg(x_144, x_143);
lean_dec(x_144);
x_150 = l_Lean_Parser_Tactic_Conv_arg___closed__6;
x_150 = l_Lean_Parser_Tactic_Conv_convSeq1Indented___closed__12;
lean_inc(x_149);
x_151 = l_Lean_Syntax_isOfKind(x_149, x_150);
if (x_151 == 0)
@ -5669,53 +5745,199 @@ return x_185;
else
{
lean_object* x_186; uint8_t x_187;
x_186 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(x_2, x_3);
x_187 = !lean_is_exclusive(x_186);
x_186 = l_Lean_Syntax_getArg(x_149, x_143);
lean_inc(x_186);
x_187 = l_Lean_Syntax_isNodeOf(x_186, x_10, x_143);
if (x_187 == 0)
{
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;
x_188 = lean_ctor_get(x_186, 0);
x_189 = l_Lean_Parser_Tactic_Conv_arg___closed__1;
x_190 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_190, 0, x_188);
lean_ctor_set(x_190, 1, x_189);
x_191 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__6;
x_192 = lean_array_push(x_191, x_190);
x_193 = lean_array_push(x_192, x_149);
x_194 = lean_box(2);
x_195 = l_Lean_Parser_Tactic_Conv_arg___closed__2;
x_196 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_196, 0, x_194);
lean_ctor_set(x_196, 1, x_195);
lean_ctor_set(x_196, 2, x_193);
lean_ctor_set(x_186, 0, x_196);
return x_186;
uint8_t x_188;
x_188 = l_Lean_Syntax_isNodeOf(x_186, x_10, x_11);
if (x_188 == 0)
{
lean_object* x_189; lean_object* x_190;
lean_dec(x_149);
lean_dec(x_2);
x_189 = lean_box(1);
x_190 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_190, 0, x_189);
lean_ctor_set(x_190, 1, x_3);
return x_190;
}
else
{
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;
x_197 = lean_ctor_get(x_186, 0);
x_198 = lean_ctor_get(x_186, 1);
lean_inc(x_198);
lean_inc(x_197);
lean_dec(x_186);
lean_object* x_191; lean_object* x_192; uint8_t x_193;
x_191 = l_Lean_Syntax_getArg(x_149, x_11);
lean_dec(x_149);
x_192 = l_Lean_Parser_Tactic_Conv_arg___closed__10;
lean_inc(x_191);
x_193 = l_Lean_Syntax_isOfKind(x_191, x_192);
if (x_193 == 0)
{
lean_object* x_194; lean_object* x_195;
lean_dec(x_191);
lean_dec(x_2);
x_194 = lean_box(1);
x_195 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_195, 0, x_194);
lean_ctor_set(x_195, 1, x_3);
return x_195;
}
else
{
lean_object* x_196; uint8_t x_197;
x_196 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(x_2, x_3);
x_197 = !lean_is_exclusive(x_196);
if (x_197 == 0)
{
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;
x_198 = lean_ctor_get(x_196, 0);
x_199 = l_Lean_Parser_Tactic_Conv_arg___closed__1;
lean_inc(x_198);
x_200 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_200, 0, x_197);
lean_ctor_set(x_200, 0, x_198);
lean_ctor_set(x_200, 1, x_199);
x_201 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__6;
x_202 = lean_array_push(x_201, x_200);
x_203 = lean_array_push(x_202, x_149);
x_204 = lean_box(2);
x_205 = l_Lean_Parser_Tactic_Conv_arg___closed__2;
x_206 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_206, 0, x_204);
lean_ctor_set(x_206, 1, x_205);
lean_ctor_set(x_206, 2, x_203);
x_207 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_207, 0, x_206);
lean_ctor_set(x_207, 1, x_198);
return x_207;
x_201 = l_Lean_Parser_Tactic_Conv_arg___closed__5;
x_202 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_202, 0, x_198);
lean_ctor_set(x_202, 1, x_201);
x_203 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__7;
x_204 = lean_array_push(x_203, x_202);
x_205 = lean_box(2);
x_206 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__2;
x_207 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_207, 0, x_205);
lean_ctor_set(x_207, 1, x_206);
lean_ctor_set(x_207, 2, x_204);
x_208 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__3;
x_209 = lean_array_push(x_208, x_200);
x_210 = lean_array_push(x_209, x_207);
x_211 = lean_array_push(x_210, x_191);
x_212 = l_Lean_Parser_Tactic_Conv_arg___closed__2;
x_213 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_213, 0, x_205);
lean_ctor_set(x_213, 1, x_212);
lean_ctor_set(x_213, 2, x_211);
lean_ctor_set(x_196, 0, x_213);
return x_196;
}
else
{
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;
x_214 = lean_ctor_get(x_196, 0);
x_215 = lean_ctor_get(x_196, 1);
lean_inc(x_215);
lean_inc(x_214);
lean_dec(x_196);
x_216 = l_Lean_Parser_Tactic_Conv_arg___closed__1;
lean_inc(x_214);
x_217 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_217, 0, x_214);
lean_ctor_set(x_217, 1, x_216);
x_218 = l_Lean_Parser_Tactic_Conv_arg___closed__5;
x_219 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_219, 0, x_214);
lean_ctor_set(x_219, 1, x_218);
x_220 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__7;
x_221 = lean_array_push(x_220, x_219);
x_222 = lean_box(2);
x_223 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__2;
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_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__3;
x_226 = lean_array_push(x_225, x_217);
x_227 = lean_array_push(x_226, x_224);
x_228 = lean_array_push(x_227, x_191);
x_229 = l_Lean_Parser_Tactic_Conv_arg___closed__2;
x_230 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_230, 0, x_222);
lean_ctor_set(x_230, 1, x_229);
lean_ctor_set(x_230, 2, x_228);
x_231 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_231, 0, x_230);
lean_ctor_set(x_231, 1, x_215);
return x_231;
}
}
}
}
else
{
lean_object* x_232; lean_object* x_233; uint8_t x_234;
lean_dec(x_186);
x_232 = l_Lean_Syntax_getArg(x_149, x_11);
lean_dec(x_149);
x_233 = l_Lean_Parser_Tactic_Conv_arg___closed__10;
lean_inc(x_232);
x_234 = l_Lean_Syntax_isOfKind(x_232, x_233);
if (x_234 == 0)
{
lean_object* x_235; lean_object* x_236;
lean_dec(x_232);
lean_dec(x_2);
x_235 = lean_box(1);
x_236 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_236, 0, x_235);
lean_ctor_set(x_236, 1, x_3);
return x_236;
}
else
{
lean_object* x_237; uint8_t x_238;
x_237 = l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______macroRules__precMax__1___spec__1(x_2, x_3);
x_238 = !lean_is_exclusive(x_237);
if (x_238 == 0)
{
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;
x_239 = lean_ctor_get(x_237, 0);
x_240 = l_Lean_Parser_Tactic_Conv_arg___closed__1;
x_241 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_241, 0, x_239);
lean_ctor_set(x_241, 1, x_240);
x_242 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__3;
x_243 = lean_array_push(x_242, x_241);
x_244 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__5;
x_245 = lean_array_push(x_243, x_244);
x_246 = lean_array_push(x_245, x_232);
x_247 = lean_box(2);
x_248 = l_Lean_Parser_Tactic_Conv_arg___closed__2;
x_249 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_249, 0, x_247);
lean_ctor_set(x_249, 1, x_248);
lean_ctor_set(x_249, 2, x_246);
lean_ctor_set(x_237, 0, x_249);
return x_237;
}
else
{
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;
x_250 = lean_ctor_get(x_237, 0);
x_251 = lean_ctor_get(x_237, 1);
lean_inc(x_251);
lean_inc(x_250);
lean_dec(x_237);
x_252 = l_Lean_Parser_Tactic_Conv_arg___closed__1;
x_253 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_253, 0, x_250);
lean_ctor_set(x_253, 1, x_252);
x_254 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__3;
x_255 = lean_array_push(x_254, x_253);
x_256 = l_Lean_Parser_Tactic_Conv___aux__Init__Conv______macroRules__Lean__Parser__Tactic__Conv__conv_xb7_x2e____1___closed__5;
x_257 = lean_array_push(x_255, x_256);
x_258 = lean_array_push(x_257, x_232);
x_259 = lean_box(2);
x_260 = l_Lean_Parser_Tactic_Conv_arg___closed__2;
x_261 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_261, 0, x_259);
lean_ctor_set(x_261, 1, x_260);
lean_ctor_set(x_261, 2, x_258);
x_262 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_262, 0, x_261);
lean_ctor_set(x_262, 1, x_251);
return x_262;
}
}
}
}
}
@ -7568,6 +7790,14 @@ l_Lean_Parser_Tactic_Conv_arg___closed__8 = _init_l_Lean_Parser_Tactic_Conv_arg_
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_arg___closed__8);
l_Lean_Parser_Tactic_Conv_arg___closed__9 = _init_l_Lean_Parser_Tactic_Conv_arg___closed__9();
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_arg___closed__9);
l_Lean_Parser_Tactic_Conv_arg___closed__10 = _init_l_Lean_Parser_Tactic_Conv_arg___closed__10();
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_arg___closed__10);
l_Lean_Parser_Tactic_Conv_arg___closed__11 = _init_l_Lean_Parser_Tactic_Conv_arg___closed__11();
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_arg___closed__11);
l_Lean_Parser_Tactic_Conv_arg___closed__12 = _init_l_Lean_Parser_Tactic_Conv_arg___closed__12();
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_arg___closed__12);
l_Lean_Parser_Tactic_Conv_arg___closed__13 = _init_l_Lean_Parser_Tactic_Conv_arg___closed__13();
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_arg___closed__13);
l_Lean_Parser_Tactic_Conv_arg = _init_l_Lean_Parser_Tactic_Conv_arg();
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_arg);
l_Lean_Parser_Tactic_Conv_ext___closed__1 = _init_l_Lean_Parser_Tactic_Conv_ext___closed__1();
@ -8006,6 +8236,10 @@ l_Lean_Parser_Tactic_Conv_enterArg___closed__3 = _init_l_Lean_Parser_Tactic_Conv
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_enterArg___closed__3);
l_Lean_Parser_Tactic_Conv_enterArg___closed__4 = _init_l_Lean_Parser_Tactic_Conv_enterArg___closed__4();
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_enterArg___closed__4);
l_Lean_Parser_Tactic_Conv_enterArg___closed__5 = _init_l_Lean_Parser_Tactic_Conv_enterArg___closed__5();
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_enterArg___closed__5);
l_Lean_Parser_Tactic_Conv_enterArg___closed__6 = _init_l_Lean_Parser_Tactic_Conv_enterArg___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_enterArg___closed__6);
l_Lean_Parser_Tactic_Conv_enterArg = _init_l_Lean_Parser_Tactic_Conv_enterArg();
lean_mark_persistent(l_Lean_Parser_Tactic_Conv_enterArg);
l_Lean_Parser_Tactic_Conv_convEnter_x5b_____x5d___closed__1 = _init_l_Lean_Parser_Tactic_Conv_convEnter_x5b_____x5d___closed__1();

2135
stage0/stdlib/Lean/Elab/Tactic/Conv/Congr.c generated
View file

File diff suppressed because it is too large Load diff

770
stage0/stdlib/Lean/Elab/Tactic/Induction.c generated
View file

@ -16,7 +16,6 @@ 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;
@ -40,7 +39,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_7101_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7413_(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;
@ -95,9 +94,11 @@ lean_object* l_List_filterMap___at_Lean_resolveGlobalConst___spec__1(lean_object
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__1(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___lambda__1___closed__1;
lean_object* l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Tactic_adaptExpander___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___lambda__2(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCases___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_saveState___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTacticAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkMVar(lean_object*);
lean_object* lean_environment_find(lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec__5___lambda__2___closed__6;
@ -118,6 +119,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_setMotiveArg___lambda__1___b
static lean_object* l_Lean_Elab_Tactic_ElimApp_setMotiveArg___closed__6;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltVarNames(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___closed__1;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_go___lambda__2___closed__3;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -141,6 +143,7 @@ lean_object* l_Lean_Elab_InfoTree_substitute(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_withMainContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_resolveGlobalConstNoOverload___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___spec__2___closed__2;
LEAN_EXPORT lean_object* l_Std_PersistentArray_mapM___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f(lean_object*);
static lean_object* l_Lean_Elab_Tactic_getInductiveValFromMajor___lambda__1___closed__1;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__2___closed__2;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec__5___lambda__1___boxed(lean_object**);
@ -150,6 +153,7 @@ static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Ind
static lean_object* l_Lean_Elab_Tactic_evalInduction___lambda__2___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getArgExpectedType(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec__5___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__2(lean_object*, size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_mkElimApp___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getFirstAltLhs___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___boxed__const__1;
@ -191,9 +195,11 @@ static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_g
extern lean_object* l_Lean_LocalContext_empty;
static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___lambda__3(lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange___closed__7;
lean_object* l_List_mapTRAux___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___lambda__2___boxed(lean_object**);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandCases_x3f(lean_object*);
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*);
@ -291,6 +297,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___lambda__1___boxed(le
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec__5___lambda__2___closed__8;
lean_object* l_Std_RBNode_insert___at_Lean_Meta_ToHide_moveToHiddeProp___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalInduction___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAlt___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
@ -347,6 +354,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tac
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___spec__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__1(lean_object*, size_t, size_t);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -450,6 +458,7 @@ lean_object* l_Lean_Meta_Cases_unifyEqs_x3f(lean_object*, lean_object*, lean_obj
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___lambda__4(lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_saveAltVarsInfo___boxed__const__1;
lean_object* l_Lean_Meta_getCustomEliminator_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInduction_x3f(lean_object*);
static lean_object* l_Lean_resolveGlobalConstNoOverload___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___spec__2___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeTargets___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprMVarAssigned(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -541,6 +550,7 @@ LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Tact
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn(lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7413____closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getBindingName___boxed(lean_object*);
lean_object* l_Array_findIdx_x3f_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___lambda__1___closed__2;
@ -600,116 +610,6 @@ 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_isMultiAlt(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6;
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) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
static lean_object* _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_usize_dec_lt(x_3, x_2);
if (x_5 == 0)
{
lean_dec(x_1);
return x_4;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; size_t x_15; size_t x_16; lean_object* x_17;
x_6 = lean_array_uget(x_4, x_3);
x_7 = lean_unsigned_to_nat(0u);
x_8 = lean_array_uset(x_4, x_3, x_7);
x_9 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1;
x_10 = lean_array_push(x_9, x_6);
x_11 = lean_box(2);
x_12 = l_Lean_nullKind;
x_13 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
lean_ctor_set(x_13, 2, x_10);
lean_inc(x_1);
x_14 = l_Lean_Syntax_setArg(x_1, x_7, x_13);
x_15 = 1;
x_16 = lean_usize_add(x_3, x_15);
x_17 = lean_array_uset(x_8, x_3, x_14);
x_3 = x_16;
x_4 = x_17;
goto _start;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f(lean_object* x_1) {
_start:
{
uint8_t x_2;
x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(x_1);
if (x_2 == 0)
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_box(0);
return x_3;
}
else
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; size_t x_8; size_t x_9; lean_object* x_10; lean_object* x_11;
x_4 = lean_unsigned_to_nat(0u);
x_5 = l_Lean_Syntax_getArg(x_1, x_4);
x_6 = l_Lean_Syntax_getArgs(x_5);
lean_dec(x_5);
x_7 = lean_array_get_size(x_6);
x_8 = lean_usize_of_nat(x_7);
lean_dec(x_7);
x_9 = 0;
x_10 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1(x_1, x_8, x_9, x_6);
x_11 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_11, 0, x_10);
return x_11;
}
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_7 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1(x_1, x_5, x_6, x_4);
return x_7;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getFirstAltLhs(lean_object* x_1) {
_start:
{
@ -13214,6 +13114,430 @@ lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT uint8_t l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(lean_object* x_1) {
_start:
{
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) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
static lean_object* _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_usize_dec_lt(x_3, x_2);
if (x_5 == 0)
{
lean_dec(x_1);
return x_4;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; size_t x_15; size_t x_16; lean_object* x_17;
x_6 = lean_array_uget(x_4, x_3);
x_7 = lean_unsigned_to_nat(0u);
x_8 = lean_array_uset(x_4, x_3, x_7);
x_9 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1;
x_10 = lean_array_push(x_9, x_6);
x_11 = lean_box(2);
x_12 = l_Lean_nullKind;
x_13 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
lean_ctor_set(x_13, 2, x_10);
lean_inc(x_1);
x_14 = l_Lean_Syntax_setArg(x_1, x_7, x_13);
x_15 = 1;
x_16 = lean_usize_add(x_3, x_15);
x_17 = lean_array_uset(x_8, x_3, x_14);
x_3 = x_16;
x_4 = x_17;
goto _start;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f(lean_object* x_1) {
_start:
{
uint8_t x_2;
x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(x_1);
if (x_2 == 0)
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_box(0);
return x_3;
}
else
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; size_t x_8; size_t x_9; lean_object* x_10; lean_object* x_11;
x_4 = lean_unsigned_to_nat(0u);
x_5 = l_Lean_Syntax_getArg(x_1, x_4);
x_6 = l_Lean_Syntax_getArgs(x_5);
lean_dec(x_5);
x_7 = lean_array_get_size(x_6);
x_8 = lean_usize_of_nat(x_7);
lean_dec(x_7);
x_9 = 0;
x_10 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1(x_1, x_8, x_9, x_6);
x_11 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_11, 0, x_10);
return x_11;
}
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_7 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1(x_1, x_5, x_6, x_4);
return x_7;
}
}
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__1(lean_object* x_1, size_t x_2, size_t x_3) {
_start:
{
uint8_t x_4;
x_4 = lean_usize_dec_eq(x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5; uint8_t x_6;
x_5 = lean_array_uget(x_1, x_2);
x_6 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_isMultiAlt(x_5);
lean_dec(x_5);
if (x_6 == 0)
{
size_t x_7; size_t x_8;
x_7 = 1;
x_8 = lean_usize_add(x_2, x_7);
x_2 = x_8;
goto _start;
}
else
{
uint8_t x_10;
x_10 = 1;
return x_10;
}
}
else
{
uint8_t x_11;
x_11 = 0;
return x_11;
}
}
}
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__2(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_usize_dec_lt(x_3, x_2);
if (x_5 == 0)
{
return x_4;
}
else
{
lean_object* x_6; lean_object* x_7;
x_6 = lean_array_uget(x_1, x_3);
lean_inc(x_6);
x_7 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f(x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; size_t x_9; size_t x_10;
x_8 = lean_array_push(x_4, x_6);
x_9 = 1;
x_10 = lean_usize_add(x_3, x_9);
x_3 = x_10;
x_4 = x_8;
goto _start;
}
else
{
lean_object* x_12; lean_object* x_13; size_t x_14; size_t x_15;
lean_dec(x_6);
x_12 = lean_ctor_get(x_7, 0);
lean_inc(x_12);
lean_dec(x_7);
x_13 = l_Array_append___rarg(x_4, x_12);
x_14 = 1;
x_15 = lean_usize_add(x_3, x_14);
x_3 = x_15;
x_4 = x_13;
goto _start;
}
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_2 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfInductionAlts(x_1);
x_3 = lean_array_get_size(x_2);
x_4 = lean_unsigned_to_nat(0u);
x_5 = lean_nat_dec_lt(x_4, x_3);
if (x_5 == 0)
{
lean_object* x_6;
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_6 = lean_box(0);
return x_6;
}
else
{
uint8_t x_7;
x_7 = lean_nat_dec_le(x_3, x_3);
if (x_7 == 0)
{
lean_object* x_8;
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_8 = lean_box(0);
return x_8;
}
else
{
size_t x_9; size_t x_10; uint8_t x_11;
x_9 = 0;
x_10 = lean_usize_of_nat(x_3);
lean_dec(x_3);
x_11 = l_Array_anyMUnsafe_any___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__1(x_2, x_9, x_10);
if (x_11 == 0)
{
lean_object* x_12;
lean_dec(x_2);
lean_dec(x_1);
x_12 = lean_box(0);
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_13 = l_Lean_Elab_Tactic_ElimApp_State_alts___default___closed__1;
x_14 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__2(x_2, x_10, x_9, x_13);
lean_dec(x_2);
x_15 = lean_box(2);
x_16 = l_Lean_nullKind;
x_17 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_17, 0, x_15);
lean_ctor_set(x_17, 1, x_16);
lean_ctor_set(x_17, 2, x_14);
x_18 = lean_unsigned_to_nat(2u);
x_19 = l_Lean_Syntax_setArg(x_1, x_18, x_17);
x_20 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_20, 0, x_19);
return x_20;
}
}
}
}
}
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; uint8_t x_6; lean_object* x_7;
x_4 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_5 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_6 = l_Array_anyMUnsafe_any___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__1(x_1, x_4, x_5);
lean_dec(x_1);
x_7 = lean_box(x_6);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_7 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f___spec__2(x_1, x_5, x_6, x_4);
lean_dec(x_1);
return x_7;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInduction_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = lean_unsigned_to_nat(4u);
x_3 = l_Lean_Syntax_getArg(x_1, x_2);
x_4 = l_Lean_Syntax_isNone(x_3);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_unsigned_to_nat(0u);
x_6 = l_Lean_Syntax_getArg(x_3, x_5);
lean_dec(x_3);
x_7 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f(x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8;
lean_dec(x_1);
x_8 = lean_box(0);
return x_8;
}
else
{
uint8_t x_9;
x_9 = !lean_is_exclusive(x_7);
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_10 = lean_ctor_get(x_7, 0);
x_11 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1;
x_12 = lean_array_push(x_11, x_10);
x_13 = lean_box(2);
x_14 = l_Lean_nullKind;
x_15 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
lean_ctor_set(x_15, 2, x_12);
x_16 = l_Lean_Syntax_setArg(x_1, x_2, x_15);
lean_ctor_set(x_7, 0, x_16);
return x_7;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_17 = lean_ctor_get(x_7, 0);
lean_inc(x_17);
lean_dec(x_7);
x_18 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1;
x_19 = lean_array_push(x_18, x_17);
x_20 = lean_box(2);
x_21 = l_Lean_nullKind;
x_22 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
lean_ctor_set(x_22, 2, x_19);
x_23 = l_Lean_Syntax_setArg(x_1, x_2, x_22);
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_23);
return x_24;
}
}
}
else
{
lean_object* x_25;
lean_dec(x_3);
lean_dec(x_1);
x_25 = lean_box(0);
return x_25;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandCases_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = lean_unsigned_to_nat(3u);
x_3 = l_Lean_Syntax_getArg(x_1, x_2);
x_4 = l_Lean_Syntax_isNone(x_3);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_unsigned_to_nat(0u);
x_6 = l_Lean_Syntax_getArg(x_3, x_5);
lean_dec(x_3);
x_7 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInductionAlts_x3f(x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8;
lean_dec(x_1);
x_8 = lean_box(0);
return x_8;
}
else
{
uint8_t x_9;
x_9 = !lean_is_exclusive(x_7);
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_10 = lean_ctor_get(x_7, 0);
x_11 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1;
x_12 = lean_array_push(x_11, x_10);
x_13 = lean_box(2);
x_14 = l_Lean_nullKind;
x_15 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
lean_ctor_set(x_15, 2, x_12);
x_16 = l_Lean_Syntax_setArg(x_1, x_2, x_15);
lean_ctor_set(x_7, 0, x_16);
return x_7;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_17 = lean_ctor_get(x_7, 0);
lean_inc(x_17);
lean_dec(x_7);
x_18 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1;
x_19 = lean_array_push(x_18, x_17);
x_20 = lean_box(2);
x_21 = l_Lean_nullKind;
x_22 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
lean_ctor_set(x_22, 2, x_19);
x_23 = l_Lean_Syntax_setArg(x_1, x_2, x_22);
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_23);
return x_24;
}
}
}
else
{
lean_object* x_25;
lean_dec(x_3);
lean_dec(x_1);
x_25 = lean_box(0);
return x_25;
}
}
}
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__1___closed__1() {
_start:
{
@ -18117,6 +18441,80 @@ return x_71;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction___lambda__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
uint8_t x_12;
x_12 = !lean_is_exclusive(x_5);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_13 = lean_ctor_get(x_5, 1);
lean_inc(x_2);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_1);
lean_ctor_set(x_14, 1, x_2);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
lean_ctor_set(x_5, 1, x_15);
x_16 = l_Lean_Elab_Tactic_evalTacticAux(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18; uint8_t x_19; uint8_t x_20; uint8_t x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26; uint8_t x_27; uint8_t x_28; uint8_t x_29; lean_object* x_30; uint8_t x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_17 = lean_ctor_get(x_5, 0);
x_18 = lean_ctor_get(x_5, 1);
x_19 = lean_ctor_get_uint8(x_5, sizeof(void*)*7);
x_20 = lean_ctor_get_uint8(x_5, sizeof(void*)*7 + 1);
x_21 = lean_ctor_get_uint8(x_5, sizeof(void*)*7 + 2);
x_22 = lean_ctor_get(x_5, 2);
x_23 = lean_ctor_get(x_5, 3);
x_24 = lean_ctor_get(x_5, 4);
x_25 = lean_ctor_get(x_5, 5);
x_26 = lean_ctor_get_uint8(x_5, sizeof(void*)*7 + 3);
x_27 = lean_ctor_get_uint8(x_5, sizeof(void*)*7 + 4);
x_28 = lean_ctor_get_uint8(x_5, sizeof(void*)*7 + 5);
x_29 = lean_ctor_get_uint8(x_5, sizeof(void*)*7 + 6);
x_30 = lean_ctor_get(x_5, 6);
x_31 = lean_ctor_get_uint8(x_5, sizeof(void*)*7 + 7);
lean_inc(x_30);
lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_inc(x_22);
lean_inc(x_18);
lean_inc(x_17);
lean_dec(x_5);
lean_inc(x_2);
x_32 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_32, 0, x_1);
lean_ctor_set(x_32, 1, x_2);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_18);
x_34 = lean_alloc_ctor(0, 7, 8);
lean_ctor_set(x_34, 0, x_17);
lean_ctor_set(x_34, 1, x_33);
lean_ctor_set(x_34, 2, x_22);
lean_ctor_set(x_34, 3, x_23);
lean_ctor_set(x_34, 4, x_24);
lean_ctor_set(x_34, 5, x_25);
lean_ctor_set(x_34, 6, x_30);
lean_ctor_set_uint8(x_34, sizeof(void*)*7, x_19);
lean_ctor_set_uint8(x_34, sizeof(void*)*7 + 1, x_20);
lean_ctor_set_uint8(x_34, sizeof(void*)*7 + 2, x_21);
lean_ctor_set_uint8(x_34, sizeof(void*)*7 + 3, x_26);
lean_ctor_set_uint8(x_34, sizeof(void*)*7 + 4, x_27);
lean_ctor_set_uint8(x_34, sizeof(void*)*7 + 5, x_28);
lean_ctor_set_uint8(x_34, sizeof(void*)*7 + 6, x_29);
lean_ctor_set_uint8(x_34, sizeof(void*)*7 + 7, x_31);
x_35 = l_Lean_Elab_Tactic_evalTacticAux(x_2, x_3, x_4, x_34, x_6, x_7, x_8, x_9, x_10, x_11);
return x_35;
}
}
}
static lean_object* _init_l_Lean_Elab_Tactic_evalInduction___boxed__const__1() {
_start:
{
@ -18129,32 +18527,52 @@ return x_2;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalInduction(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; size_t x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_11 = lean_unsigned_to_nat(4u);
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
x_13 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfOptInductionAlts(x_12);
x_14 = lean_unsigned_to_nat(1u);
x_15 = l_Lean_Syntax_getArg(x_1, x_14);
x_16 = l_Lean_Syntax_getSepArgs(x_15);
x_17 = lean_array_get_size(x_16);
x_18 = lean_usize_of_nat(x_17);
lean_dec(x_17);
x_19 = lean_box_usize(x_18);
x_20 = l_Lean_Elab_Tactic_evalInduction___boxed__const__1;
x_21 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_evalInduction___spec__1___boxed), 12, 3);
lean_closure_set(x_21, 0, x_19);
lean_closure_set(x_21, 1, x_20);
lean_closure_set(x_21, 2, x_16);
x_22 = l_Lean_Elab_Tactic_evalInduction___boxed__const__1;
x_23 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInduction___lambda__4___boxed), 15, 6);
lean_closure_set(x_23, 0, x_21);
lean_closure_set(x_23, 1, x_1);
lean_closure_set(x_23, 2, x_22);
lean_closure_set(x_23, 3, x_15);
lean_closure_set(x_23, 4, x_12);
lean_closure_set(x_23, 5, x_13);
x_24 = l_Lean_Elab_Tactic_focus___rarg(x_23, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_24;
lean_object* x_11;
lean_inc(x_1);
x_11 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandInduction_x3f(x_1);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; size_t x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_12 = lean_unsigned_to_nat(4u);
x_13 = l_Lean_Syntax_getArg(x_1, x_12);
x_14 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltsOfOptInductionAlts(x_13);
x_15 = lean_unsigned_to_nat(1u);
x_16 = l_Lean_Syntax_getArg(x_1, x_15);
x_17 = l_Lean_Syntax_getSepArgs(x_16);
x_18 = lean_array_get_size(x_17);
x_19 = lean_usize_of_nat(x_18);
lean_dec(x_18);
x_20 = lean_box_usize(x_19);
x_21 = l_Lean_Elab_Tactic_evalInduction___boxed__const__1;
x_22 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_evalInduction___spec__1___boxed), 12, 3);
lean_closure_set(x_22, 0, x_20);
lean_closure_set(x_22, 1, x_21);
lean_closure_set(x_22, 2, x_17);
x_23 = l_Lean_Elab_Tactic_evalInduction___boxed__const__1;
x_24 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInduction___lambda__4___boxed), 15, 6);
lean_closure_set(x_24, 0, x_22);
lean_closure_set(x_24, 1, x_1);
lean_closure_set(x_24, 2, x_23);
lean_closure_set(x_24, 3, x_16);
lean_closure_set(x_24, 4, x_13);
lean_closure_set(x_24, 5, x_14);
x_25 = l_Lean_Elab_Tactic_focus___rarg(x_24, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_25;
}
else
{
lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_26 = lean_ctor_get(x_11, 0);
lean_inc(x_26);
lean_dec(x_11);
lean_inc(x_26);
lean_inc(x_1);
x_27 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInduction___lambda__5), 11, 2);
lean_closure_set(x_27, 0, x_1);
lean_closure_set(x_27, 1, x_26);
x_28 = l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Tactic_adaptExpander___spec__1(x_1, x_26, x_27, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_28;
}
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_evalInduction___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
@ -18375,7 +18793,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(445u);
x_1 = lean_unsigned_to_nat(500u);
x_2 = lean_unsigned_to_nat(46u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -18387,7 +18805,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(477u);
x_1 = lean_unsigned_to_nat(535u);
x_2 = lean_unsigned_to_nat(92u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -18415,7 +18833,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(445u);
x_1 = lean_unsigned_to_nat(500u);
x_2 = lean_unsigned_to_nat(50u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -18427,7 +18845,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(445u);
x_1 = lean_unsigned_to_nat(500u);
x_2 = lean_unsigned_to_nat(63u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20469,16 +20887,36 @@ return x_64;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCases(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_11 = lean_unsigned_to_nat(1u);
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
x_13 = l_Lean_Syntax_getSepArgs(x_12);
x_14 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalCases___lambda__3___boxed), 12, 3);
lean_closure_set(x_14, 0, x_13);
lean_closure_set(x_14, 1, x_1);
lean_closure_set(x_14, 2, x_12);
x_15 = l_Lean_Elab_Tactic_focus___rarg(x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_15;
lean_object* x_11;
lean_inc(x_1);
x_11 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandCases_x3f(x_1);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_12 = lean_unsigned_to_nat(1u);
x_13 = l_Lean_Syntax_getArg(x_1, x_12);
x_14 = l_Lean_Syntax_getSepArgs(x_13);
x_15 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalCases___lambda__3___boxed), 12, 3);
lean_closure_set(x_15, 0, x_14);
lean_closure_set(x_15, 1, x_1);
lean_closure_set(x_15, 2, x_13);
x_16 = l_Lean_Elab_Tactic_focus___rarg(x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = lean_ctor_get(x_11, 0);
lean_inc(x_17);
lean_dec(x_11);
lean_inc(x_17);
lean_inc(x_1);
x_18 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalInduction___lambda__5), 11, 2);
lean_closure_set(x_18, 0, x_1);
lean_closure_set(x_18, 1, x_17);
x_19 = l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Tactic_adaptExpander___spec__1(x_1, x_17, x_18, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_19;
}
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_evalCases___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
@ -20623,7 +21061,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(501u);
x_1 = lean_unsigned_to_nat(559u);
x_2 = lean_unsigned_to_nat(42u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20635,8 +21073,8 @@ 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(524u);
x_2 = lean_unsigned_to_nat(116u);
x_1 = lean_unsigned_to_nat(585u);
x_2 = lean_unsigned_to_nat(118u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -20650,7 +21088,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
x_1 = l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange___closed__1;
x_2 = lean_unsigned_to_nat(42u);
x_3 = l___regBuiltin_Lean_Elab_Tactic_evalCases_declRange___closed__2;
x_4 = lean_unsigned_to_nat(116u);
x_4 = lean_unsigned_to_nat(118u);
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
@ -20663,7 +21101,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(501u);
x_1 = lean_unsigned_to_nat(559u);
x_2 = lean_unsigned_to_nat(46u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20675,7 +21113,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(501u);
x_1 = lean_unsigned_to_nat(559u);
x_2 = lean_unsigned_to_nat(55u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -20721,7 +21159,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_7101____closed__1() {
static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7413____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -20731,11 +21169,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_7101_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7413_(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_7101____closed__1;
x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7413____closed__1;
x_3 = l_Lean_registerTraceClass(x_2, x_1);
if (lean_obj_tag(x_3) == 0)
{
@ -20824,8 +21262,6 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_Tactic_Generalize(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1 = _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1();
lean_mark_persistent(l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1);
l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__1 = _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__1);
l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__2 = _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltName___closed__2();
@ -20970,6 +21406,8 @@ l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___closed__2);
l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getOptPreTacOfOptInductionAlts___closed__1 = _init_l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getOptPreTacOfOptInductionAlts___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getOptPreTacOfOptInductionAlts___closed__1);
l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1 = _init_l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1();
lean_mark_persistent(l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_expandMultiAlt_x3f___spec__1___closed__1);
l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__1___closed__1 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__1___closed__1();
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__1___closed__1);
l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__2___closed__1 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__2___closed__1();
@ -21118,9 +21556,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_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());
l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7413____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7413____closed__1();
lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7413____closed__1);
res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Induction___hyg_7413_(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));

2
stage0/stdlib/Lean/Linter/Basic.c generated
View file

@ -3132,7 +3132,7 @@ static lean_object* _init_l_List_foldr___at_Lean_Linter_unusedVariables_isPatter
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("inductionAlt", 12);
x_1 = lean_mk_string_from_bytes("inductionAltLHS", 15);
return x_1;
}
}

1525
stage0/stdlib/Lean/Parser/Command.c generated
View file

File diff suppressed because it is too large Load diff