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

chore: unused variables at Simp.lean

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-06 18:24:10 -07:00
parent 71226243fd
commit 875e71a0d7
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Elab/Tactic/Simp.lean
View file

@ -287,17 +287,17 @@ where
| none => replaceMainGoal []
| some mvarId => replaceMainGoal [mvarId]
def dsimpLocation (ctx : Simp.Context) (fvarIdToSimp : FVarIdToLemmaId := {}) (loc : Location) : TacticM Unit := do
def dsimpLocation (ctx : Simp.Context) (loc : Location) : TacticM Unit := do
match loc with
| Location.targets hyps simplifyTarget =>
withMainContext do
let fvarIds ← getFVarIds hyps
go fvarIds simplifyTarget fvarIdToSimp
go fvarIds simplifyTarget
| Location.wildcard =>
withMainContext do
go (← getNondepPropHyps (← getMainGoal)) (simplifyTarget := true) fvarIdToSimp
go (← getNondepPropHyps (← getMainGoal)) (simplifyTarget := true)
where
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToSimp : Lean.Meta.FVarIdToLemmaId) : TacticM Unit := do
go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do
let mvarId ← getMainGoal
let result? ← dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
match result? with
@ -305,7 +305,7 @@ where
| some mvarId => replaceMainGoal [mvarId]
@[builtinTactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do
let { ctx, fvarIdToLemmaId, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
dsimpLocation ctx fvarIdToLemmaId (expandOptLocation stx[5])
let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
dsimpLocation ctx (expandOptLocation stx[5])
end Lean.Elab.Tactic