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

fix: instantiate mvars in rewrite tactic

Browse source
This commit is contained in:
Gabriel Ebner 2021-06-11 09:51:01 +02:00 • committed by Leonardo de Moura
parent cc2f483951
commit 94e299a730
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Rewrite.lean
View file

@ -20,7 +20,7 @@ def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
(symm : Bool := false) (occs : Occurrences := Occurrences.all) (mode := TransparencyMode.reducible) : MetaM RewriteResult :=
withMVarContext mvarId do
checkNotAssigned mvarId `rewrite
let heqType ← inferType heq
let heqType ← instantiateMVars (← inferType heq)
let (newMVars, binderInfos, heqType) ← forallMetaTelescopeReducing heqType
let heq := mkAppN heq newMVars
let cont (heq heqType : Expr) : MetaM RewriteResult := do

6
tests/lean/run/rw_inst_mvars.lean Normal file
View file

@ -0,0 +1,6 @@
example (p : Nat → Prop) (h : ∀ n, p (n+1) = p n) : (p m ↔ p 0) := by
induction m
case succ ih =>
rw [h, ih]
exact Iff.rfl
case zero => exact Iff.rfl