From 1e13c26de3efd98c63f3232b4dade6092f91f795 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 7 Mar 2021 10:22:27 -0800 Subject: [PATCH] chore: prepare to change `inductionAlts` --- src/Lean/Elab/Tactic/Induction.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 46c7a99954..86c8c2065f 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -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]