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

chore: remove unnecessary group

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-03 05:57:30 -08:00
parent f56d81de32
commit 9494552d82
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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]

2
src/Lean/Parser/Tactic.lean
View file

@ -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" >> "| ")