Lean4
/-- `modifyMetavarDecl mvarId f` updates the `MetavarDecl` for `mvarId` with `f`.
Conditions on `f`:
- The target of `f mdecl` is defeq to the target of `mdecl`.
- The local context of `f mdecl` must contain the same fvars as the local
context of `mdecl`. For each fvar in the local context of `f mdecl`, the type
(and value, if any) of the fvar must be defeq to the corresponding fvar in
the local context of `mdecl`.
If `mvarId` does not refer to a declared metavariable, nothing happens.
-/
def modifyMetavarDecl [MonadMCtx m] (mvarId : MVarId) (f : MetavarDecl → MetavarDecl) : m Unit :=
modifyMCtx fun mctx ↦
match mctx.decls.find? mvarId with
| none => mctx
| some mdecl => { mctx with decls := mctx.decls.insert mvarId (f mdecl) }
