From 94e299a730358de5dcfdf748cff81c5d37a97011 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 11 Jun 2021 09:51:01 +0200 Subject: [PATCH] fix: instantiate mvars in rewrite tactic --- src/Lean/Meta/Tactic/Rewrite.lean | 2 +- tests/lean/run/rw_inst_mvars.lean | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/rw_inst_mvars.lean diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean index f057ee311d..d605f7634c 100644 --- a/src/Lean/Meta/Tactic/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Rewrite.lean @@ -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 diff --git a/tests/lean/run/rw_inst_mvars.lean b/tests/lean/run/rw_inst_mvars.lean new file mode 100644 index 0000000000..eff45a55f5 --- /dev/null +++ b/tests/lean/run/rw_inst_mvars.lean @@ -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