Executing actions using the infotree

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

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.

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.

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.

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.