From 32f8a95437f46e42bca6900c77b7925fc76bc699 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 23 Jun 2025 18:37:18 -0700 Subject: [PATCH] fix: `Lean.MVarId.deltaLocalDecl` (#8955) This PR fixes `Lean.MVarId.deltaLocalDecl`, which previously replaced the local definition with the target. --- src/Lean/Meta/Tactic/Delta.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Tactic/Delta.lean b/src/Lean/Meta/Tactic/Delta.lean index 6ad67c299a..e27a280eb6 100644 --- a/src/Lean/Meta/Tactic/Delta.lean +++ b/src/Lean/Meta/Tactic/Delta.lean @@ -38,6 +38,6 @@ Delta expand declarations that satisfy `p` at `fvarId` type. def _root_.Lean.MVarId.deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : Name → Bool) : MetaM MVarId := mvarId.withContext do mvarId.checkNotAssigned `delta - mvarId.changeLocalDecl fvarId (← deltaExpand (← mvarId.getType) p) (checkDefEq := false) + mvarId.changeLocalDecl fvarId (← deltaExpand (← fvarId.getType) p) (checkDefEq := false) end Lean.Meta