From 73037615690df5ab5bcc4c67037b4f6fa18e7ff9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 31 May 2021 18:05:55 -0700 Subject: [PATCH] feat: add `modifyTarget` --- src/Lean/Meta/Tactic/Replace.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean index 5171638033..6d50ac8f76 100644 --- a/src/Lean/Meta/Tactic/Replace.lean +++ b/src/Lean/Meta/Tactic/Replace.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Util.ForEachExpr import Lean.Meta.AppBuilder +import Lean.Meta.MatchUtil import Lean.Meta.Tactic.Util import Lean.Meta.Tactic.Revert import Lean.Meta.Tactic.Intro @@ -102,4 +103,16 @@ def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkD | Expr.letE n t v b _ => do check t; finalize (mkLet n typeNew v b) | _ => throwTacticEx `changeHypothesis mvarId "unexpected auxiliary target" +def modifyTarget (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do + withMVarContext mvarId do + checkNotAssigned mvarId `modifyTarget + change mvarId (← f (← getMVarType mvarId)) (checkDefEq := false) + +def modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do + modifyTarget mvarId fun target => do + if let some (_, lhs, rhs) ← matchEq? target then + mkEq (← f lhs) rhs + else + throwTacticEx `modifyTargetEqLHS mvarId m!"equality expected{indentExpr target}" + end Lean.Meta