def Lean.Elab.CommandContextInfo.saveNoFileMap {m : Type → Type} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadOptions m] [MonadResolveName m] [MonadNameGenerator m] : m CommandContextInfo

def Lean.Elab.CommandContextInfo.save {m : Type → Type} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadOptions m] [MonadResolveName m] [MonadNameGenerator m] [MonadFileMap m] : m CommandContextInfo

def Lean.Elab.CustomInfo.format : CustomInfo → Format

@[instance_reducible]

instance Lean.Elab.instToFormatCustomInfo : ToFormat CustomInfo

def Lean.Elab.ContextInfo.runCoreM {α : Type} (info : ContextInfo) (x : CoreM α) : IO α

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

def Lean.Elab.ContextInfo.runMetaM {α : Type} (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α

def Lean.Elab.ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPContext

def Lean.Elab.ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) : IO Format

def Lean.Elab.TermInfo.runMetaM {α : Type} (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO α

def Lean.Elab.TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format

def Lean.Elab.PartialTermInfo.format (ctx : ContextInfo) (info : PartialTermInfo) : Format

def Lean.Elab.CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format

def Lean.Elab.CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format

def Lean.Elab.OptionInfo.format (ctx : ContextInfo) (info : OptionInfo) : IO Format

def Lean.Elab.ErrorNameInfo.format (ctx : ContextInfo) (info : ErrorNameInfo) : IO Format

def Lean.Elab.FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format

def Lean.Elab.ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO Format

def Lean.Elab.TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format

def Lean.Elab.MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format

def Lean.Elab.UserWidgetInfo.format (info : UserWidgetInfo) : Format

def Lean.Elab.FVarAliasInfo.format (info : FVarAliasInfo) : Format

def Lean.Elab.FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format

def Lean.Elab.DelabTermInfo.docString? (ppCtx : PPContext) (info : DelabTermInfo) : IO (Option String)

def Lean.Elab.DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format

def Lean.Elab.ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format

def Lean.Elab.DocInfo.format (ctx : ContextInfo) (info : DocInfo) : Format

def Lean.Elab.DocElabInfo.format (ctx : ContextInfo) (info : DocElabInfo) : Format

def Lean.Elab.Info.format (ctx : ContextInfo) : Info → IO Format

def Lean.Elab.PartialContextInfo.format (ctx : PartialContextInfo) : Format

partial def Lean.Elab.InfoTree.format (tree : InfoTree) (ctx? : Option ContextInfo := none) : IO Format

def Lean.Elab.getResetInfoTrees {m : Type → Type} [Monad m] [MonadInfoTree m] : m (PersistentArray InfoTree)

Returns the current array of InfoTrees and resets it to an empty array.

def Lean.Elab.pushInfoTree {m : Type → Type} [Monad m] [MonadInfoTree m] (t : InfoTree) : m Unit

def Lean.Elab.pushInfoLeaf {m : Type → Type} [Monad m] [MonadInfoTree m] (t : Info) : m Unit

def Lean.Elab.addCompletionInfo {m : Type → Type} [Monad m] [MonadInfoTree m] (info : CompletionInfo) : m Unit

def Lean.Elab.addConstInfo {m : Type → Type} [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadError m] (stx : Syntax) (n : Name) (expectedType? : Option Expr := none) : m Unit

def Lean.Elab.realizeGlobalConstNoOverloadWithInfo (id : Syntax) (expectedType? : Option Expr := none) : CoreM Name

This does the same job as realizeGlobalConstNoOverload; resolving an identifier syntax to a unique fully resolved name or throwing if there are ambiguities. But also adds this resolved name to the infotree. This means that when you hover over a name in the source file you will see the fully resolved name in the hover info.

def Lean.Elab.realizeGlobalConstWithInfos (id : Syntax) (expectedType? : Option Expr := none) : CoreM (List Name)

Similar to realizeGlobalConstNoOverloadWithInfo, except if there are multiple name resolutions then it returns them as a list.

def Lean.Elab.realizeGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name × List String))

Similar to realizeGlobalName, but it also adds the resolved name to the info tree.

def Lean.Elab.withInfoContext' {m : Type → Type} [Monad m] [MonadInfoTree m] {α : Type} [MonadFinally m] (x : m α) (mkInfo : α → m (Info ⊕ MVarId)) (mkInfoOnError : m Info) : m α

Adds a node containing the InfoTrees generated by x to the InfoTrees in m.

If x succeeds and mkInfo yields an Info, the InfoTrees of x become subtrees of a node containing the Info produced by mkInfo, which is then added to the InfoTrees in m. If x succeeds and mkInfo yields an MVarId, the InfoTrees of x are discarded and a hole node is added to the InfoTrees in m. If x fails, the InfoTrees of x become subtrees of a node containing the Info produced by mkInfoOnError, which is then added to the InfoTrees in m.

The InfoTrees in m are reset before x is executed and restored with the addition of a new tree after x is executed.

def Lean.Elab.withInfoTreeContext {m : Type → Type} [Monad m] [MonadInfoTree m] {α : Type} [MonadFinally m] (x : m α) (mkInfoTree : PersistentArray InfoTree → m InfoTree) : m α

Saves the current list of trees t₀, runs x to produce a new tree list t₁ and runs mkInfoTree t₁ to get n : InfoTree and then restores the trees to be t₀ ++ [n].

@[inline]

def Lean.Elab.withInfoContext {m : Type → Type} [Monad m] [MonadInfoTree m] {α : Type} [MonadFinally m] (x : m α) (mkInfo : m Info) : m α

Run x as a new child infotree node with header given by mkInfo.

def Lean.Elab.withSaveInfoContext {m : Type → Type} [Monad m] [MonadInfoTree m] {α : Type} [MonadNameGenerator m] [MonadFinally m] [MonadEnv m] [MonadOptions m] [MonadMCtx m] [MonadResolveName m] [MonadFileMap m] (x : m α) : m α

Resets the trees state t₀, runs x to produce a new trees state t₁ and sets the state to be t₀ ++ (InfoTree.context (PartialContextInfo.commandCtx Γ) <$> t₁) where Γ is the context derived from the monad state.

def Lean.Elab.withSaveParentDeclInfoContext {m : Type → Type} [Monad m] [MonadInfoTree m] {α : Type} [MonadFinally m] [MonadParentDecl m] (x : m α) : m α

Resets the trees state t₀, runs x to produce a new trees state t₁ and sets the state to be t₀ ++ (InfoTree.context (PartialContextInfo.parentDeclCtx Γ) <$> t₁) where Γ is the parent decl name provided by MonadParentDecl m.

def Lean.Elab.withSaveAutoImplicitInfoContext {m : Type → Type} [Monad m] [MonadInfoTree m] {α : Type} [MonadFinally m] [MonadAutoImplicits m] (x : m α) : m α

Resets the trees state t₀, runs x to produce a new trees state t₁ and sets the state to be t₀ ++ (InfoTree.context (PartialContextInfo.autoImplicitCtx Γ) <$> t₁) where Γ is the set of auto-implicits provided by MonadAutoImplicits m.

def Lean.Elab.getInfoHoleIdAssignment? {m : Type → Type} [Monad m] [MonadInfoTree m] (mvarId : MVarId) : m (Option InfoTree)

def Lean.Elab.assignInfoHoleId {m : Type → Type} [Monad m] [MonadInfoTree m] (mvarId : MVarId) (infoTree : InfoTree) : m Unit

def Lean.Elab.withMacroExpansionInfo {m : Type → Type} {α : Type} [MonadFinally m] [Monad m] [MonadInfoTree m] [MonadLCtx m] (stx output : Syntax) (x : m α) : m α

@[inline]

def Lean.Elab.withInfoHole {m : Type → Type} {α : Type} [MonadFinally m] [Monad m] [MonadInfoTree m] (mvarId : MVarId) (x : m α) : m α

Runs x. The last info tree that is pushed while running x is assigned to mvarId. All other pushed info trees are silently discarded.

def Lean.Elab.enableInfoTree {m : Type → Type} [MonadInfoTree m] (flag : Bool := true) : m Unit

def Lean.Elab.withEnableInfoTree {m : Type → Type} {α : Type} [Monad m] [MonadInfoTree m] [MonadFinally m] (flag : Bool) (x : m α) : m α

def Lean.Elab.getInfoTrees {m : Type → Type} [MonadInfoTree m] [Monad m] : m (PersistentArray InfoTree)