runMetaMWithMessages — Mathlib

Lean4
/-- Embeds a `MetaM` action in `CommandElabM` by supplying the information stored in `info`.

Copy of `ContextInfo.runMetaM` that makes use of the `CommandElabM` context for:
* message logging (messages produced by the `CoreM` action are migrated back),
* metavariable generation,
* auxiliary declaration generation,
* local instances.
-/
def runMetaMWithMessages (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : CommandElabM α := do
  (·.1) <$>
      info.runCoreMWithMessages
        (Lean.Meta.MetaM.run (ctx := { lctx := lctx }) (s := { mctx := info.mctx }) <|
          -- Update the local instances, otherwise typeclass search would fail to see anything in the
              -- local context.
          Meta.withLocalInstances (lctx.decls.toList.filterMap id) <| x)
Похожие утверждения