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

fix: missing goals

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-02 19:11:52 -07:00
parent 41ce24e2c6
commit 39adda8ffe
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Elab/Tactic/Conv/Rewrite.lean
View file

@ -16,6 +16,7 @@ def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx =>
let e ← elabTerm term none true
let r ← rewrite (← getMainGoal) (← getLhs) e symm (mode := mode)
updateLhs r.eNew r.eqProof
replaceMainGoal ((← getMainGoal) :: r.mvarIds)
@[builtinTactic Lean.Parser.Tactic.Conv.rewrite] def evalRewrite : Tactic :=
evalRewriteCore TransparencyMode.instances