From 9494552d82ab2fc8e3c556add2291bdebafacc10 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Nov 2020 05:57:30 -0800 Subject: [PATCH] chore: remove unnecessary `group` --- src/Lean/Elab/Tactic/Induction.lean | 6 +++--- src/Lean/Parser/Tactic.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 6e1a8a0c9e..661ba403b1 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -328,8 +328,8 @@ private partial def checkCasesResult (casesResult : Array Meta.CasesSubgoal) (ct /- Default `cases` tactic that uses `casesOn` eliminator -/ def evalCasesOn (target : Syntax) (withAlts : Syntax) : TacticM Unit := do - let h? := if target[0][0].isNone then none else some target[0][0][0].getId - let major ← elabMajor h? target[0][1] + let h? := if target[0].isNone then none else some target[0][0].getId + let major ← elabMajor h? target[1] let major ← generalizeMajor major let (mvarId, _) ← getMainGoal let (recInfo, ctorNames) ← getRecInfoDefault major withAlts true @@ -424,7 +424,7 @@ def eval (targets : Array Syntax) (elimName : Name) (withAlts : Syntax) : Tactic let elimInfo ← getElimInfo elimName let (mvarId, rest) ← getMainGoal withMVarContext mvarId do - let result ← processArgs elimName elimInfo (targets.map (·[0][1])) + let result ← processArgs elimName elimInfo (targets.map (·[1])) let elimArgs := result.elim.getAppArgs let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i] let motiveType ← inferType elimArgs[elimInfo.motivePos] diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index 5f72e8e4df..fb632ff306 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -66,7 +66,7 @@ def withAlts : Parser := optional inductionAlts def usingRec : Parser := optional (" using " >> ident) def generalizingVars := optional (" generalizing " >> many1 ident) @[builtinTacticParser] def «induction» := parser! nonReservedSymbol "induction " >> majorPremise >> usingRec >> generalizingVars >> withAlts -@[builtinTacticParser] def «cases» := parser! nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> withAlts +@[builtinTacticParser] def «cases» := parser! nonReservedSymbol "cases " >> sepBy1 majorPremise ", " >> usingRec >> withAlts def matchAlt : Parser := parser! sepBy1 termParser ", " >> darrow >> altRHS def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 matchAlt (checkColGe "alternatives must be indented" >> "| ")