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.

Equations

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

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.

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.

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.

def Lean.Elab.ContextInfo.runCoreMCapturingInfoTree {α : Type} (info : ContextInfo) (x : CoreM α) : Command.CommandElabM (α × PersistentArray InfoTree)

Embeds a CoreM action in CommandElabM, returning both the result and the InfoTrees produced.

Similar to runCoreMWithMessages but also captures InfoTrees for extracting "Try this:" suggestions.

Equations

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

def Lean.Elab.ContextInfo.runMetaMCapturingInfoTree {α : Type} (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : Command.CommandElabM (α × PersistentArray InfoTree)

Embeds a MetaM action in CommandElabM, returning both the result and InfoTrees produced.

Equations

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

def Lean.Elab.ContextInfo.runTacticCapturingInfoTree {α : Type} (ctx : ContextInfo) (i : TacticInfo) (goal : MVarId) (x : MVarId → MetaM α) : Command.CommandElabM (α × PersistentArray InfoTree)

Run a tactic computation in the context of an infotree node, capturing InfoTrees produced.

Equations

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

def Lean.Elab.ContextInfo.runTacticCodeCapturingInfoTree (ctx : ContextInfo) (i : TacticInfo) (goal : MVarId) (code : Syntax) : Command.CommandElabM (List MVarId × PersistentArray InfoTree)

Run tactic code in the context of an infotree node, capturing InfoTrees for suggestion extraction.

Returns both the resulting goals and the InfoTrees produced during tactic execution. Use collectTryThisSuggestions from Mathlib.Lean.Elab.InfoTree to extract suggestions.

Equations

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