Lean4
/-- Use the procedure `m` to rewrite hypothesis `fvarId`.
The `simpTheorems` of the simp-context carried with `m` will be modified to remove `fvarId`;
this ensures that if the procedure `m` involves rewriting by this `SimpTheoremsArray`, then, e.g.,
`h : x = y` is not transformed (by rewriting `h`) to `True`. -/
def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String) (failIfUnchanged : Bool)
(mayCloseGoal : Bool) (fvarId : FVarId) (goal : MVarId) : ReaderT Simp.Context MetaM (Option MVarId) := do
let ldecl ← fvarId.getDecl
if ldecl.isImplementationDetail then
throwError "cannot run {proc } at {ldecl.userName}, it is an implementation detail"
let tgt ← instantiateMVars (← fvarId.getType)
let eraseFVarId (ctx : Simp.Context) := ctx.setSimpTheorems <| ctx.simpTheorems.eraseTheorem (.fvar fvarId)
let r ← withReader eraseFVarId <| m tgt
if failIfUnchanged && tgt.cleanupAnnotations == r.expr.cleanupAnnotations then
throwError "{proc } made no progress at {ldecl.userName}"
return (← applySimpResultToLocalDecl goal fvarId r mayCloseGoal).map Prod.snd
