Documentation

Mathlib.Lean.ContextInfo

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.
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.
    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.

      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.

        Instances For
          source
          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.

          Instances For
            source
            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.

            Instances For
              source
              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.

              Instances For
                source
                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.

                Instances For