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

fix: missing instantiateMVars

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-02 01:17:54 -07:00
parent 4e911765eb
commit e79917d9a8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Tactic/Conv/Delta.lean
View file

@ -11,7 +11,7 @@ open Meta
@[builtinTactic Lean.Parser.Tactic.Conv.delta] def evalDelta : Tactic := fun stx => withMainContext do
let declName ← resolveGlobalConstNoOverload stx[1]
let lhsNew ← deltaExpand (← getLhs) (· == declName)
let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) (· == declName)
changeLhs lhsNew
end Lean.Elab.Tactic.Conv