# Executing actions using the infotree #

This file contains helper functions for running `CoreM`, `MetaM` and tactic actions in the context of an infotree node.

source
def Lean.Elab.ContextInfo.runCoreMWithMessages {α : Type} (info : ContextInfo) (x : CoreM α) :
Command.CommandElabM α

Embeds a `CoreM` action in `CommandElabM` by supplying the information stored in `info`.

Copy of `ContextInfo.runCoreM` that makes use of the `CommandElabM` context for:

- logging messages produced by the `CoreM` action,
- metavariable generation,
- auxiliary declaration generation.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.ContextInfo.runMetaMWithMessages {α : Type} (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) :
Command.CommandElabM α

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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.ContextInfo.runTactic {α : Type} (ctx : ContextInfo) (i : TacticInfo) (goal : MVarId) (x : MVarId → MetaM α) :
Command.CommandElabM α

Run a tactic computation in the context of an infotree node.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.ContextInfo.runTacticCode (ctx : ContextInfo) (i : TacticInfo) (goal : MVarId) (code : Syntax) (m : (α : Type) × (MVarId → MetaM α) := ⟨MVarId, pure⟩) :
Command.CommandElabM (List m.fst)

Run tactic code, given by a piece of syntax, in the context of an infotree node. The optional `MetaM` argument `m` performs postprocessing on the goals produced.

Equations

- One or more equations did not get rendered due to their size.

Instances For