Lean4
/-- Use the procedure `m` to rewrite the provided goal. -/
def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String) (failIfUnchanged : Bool)
(goal : MVarId) : ReaderT Simp.Context MetaM (Option MVarId) := do
let tgt ← instantiateMVars (← goal.getType)
let r ← m tgt
let unchanged := tgt.cleanupAnnotations == r.expr.cleanupAnnotations
if failIfUnchanged && unchanged then
throwError "{proc} made no progress on goal"
if r.expr.isTrue then
goal.assign (← mkOfEqTrue (← r.getProof))
pure none
else
-- this ensures that we really get the same goal as an `MVarId`,
-- not a different `MVarId` for which `MVarId.getType` is the same
if unchanged then
return goal
applySimpResultToTarget goal tgt r
