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

chore: prepare to change inductionAlts

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-07 10:22:27 -08:00
parent 08fc25217d
commit 1e13c26de3
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/Tactic/Induction.lean
View file

@ -243,8 +243,9 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat :
Meta.throwTacticEx `induction mvarId "major premise depends on variable being generalized"
pure (fvarIds.size, [mvarId'])
-- syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
inductionAlts[1].getArgs
inductionAlts[2].getArgs
private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]