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

Equations

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

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

Equations

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

def Lean.Elab.PartialContextInfo.mergeIntoOuter? (inner : PartialContextInfo) (outer? : Option ContextInfo) : Option ContextInfo

Merges the inner partial context into the outer context s.t. fields of the inner context overwrite fields of the outer context. Panics if the invariant described in the documentation for PartialContextInfo is violated.

When traversing an InfoTree, this function should be used to combine the context of outer nodes with the partial context of their subtrees. This ensures that the traversal has the context from the inner node to the root node of the InfoTree available, with partial contexts of inner nodes taking priority over contexts of outer nodes.

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Elab.PartialContextInfo.commandCtx info).mergeIntoOuter? none = some { toCommandContextInfo := info }
• (Lean.Elab.PartialContextInfo.commandCtx innerInfo).mergeIntoOuter? (some outer) = some { toCommandContextInfo := innerInfo, parentDecl? := outer.parentDecl? }
• (Lean.Elab.PartialContextInfo.parentDeclCtx innerParentDecl).mergeIntoOuter? (some outer) = some { toCommandContextInfo := outer.toCommandContextInfo, parentDecl? := some innerParentDecl }

def Lean.Elab.CompletionInfo.stx : CompletionInfo → Syntax

Equations

• (Lean.Elab.CompletionInfo.dot i expectedType?).stx = i.stx
• (Lean.Elab.CompletionInfo.id stx id danglingDot lctx expectedType?).stx = stx
• (Lean.Elab.CompletionInfo.dotId stx id lctx expectedType?).stx = stx
• (Lean.Elab.CompletionInfo.fieldId stx id lctx structName).stx = stx
• (Lean.Elab.CompletionInfo.namespaceId stx).stx = stx
• (Lean.Elab.CompletionInfo.option stx).stx = stx
• (Lean.Elab.CompletionInfo.endSection stx scopeNames).stx = stx
• (Lean.Elab.CompletionInfo.tactic stx).stx = stx

def Lean.Elab.CompletionInfo.lctx : CompletionInfo → LocalContext

Obtains the LocalContext from this CompletionInfo if available and yields an empty context otherwise.

Equations

• (Lean.Elab.CompletionInfo.dot i expectedType?).lctx = i.lctx
• (Lean.Elab.CompletionInfo.id stx id danglingDot lctx expectedType?).lctx = lctx
• (Lean.Elab.CompletionInfo.dotId stx id lctx expectedType?).lctx = lctx
• (Lean.Elab.CompletionInfo.fieldId stx id lctx structName).lctx = lctx
• x✝.lctx = Lean.LocalContext.empty

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

Equations

• x✝.format = Std.format "CustomInfo(" ++ Std.format x✝.value.typeName ++ Std.format ")"

instance Lean.Elab.instToFormatCustomInfo : ToFormat CustomInfo

Equations

• Lean.Elab.instToFormatCustomInfo = { format := Lean.Elab.CustomInfo.format }

partial def Lean.Elab.InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info

partial def Lean.Elab.InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMap MVarId InfoTree) : InfoTree

Instantiate the holes on the given tree with the assignment table. (analogous to instantiating the metavariables in an expression)

def Lean.Elab.InfoState.substituteLazy (s : InfoState) : Task InfoState

Applies s.lazyAssignment to s.trees, asynchronously.

Equations

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

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

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

Equations

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

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

Equations

• info.runMetaM lctx x = (fun (x : α × Lean.Meta.State) => x.fst) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })

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

Equations

• info.toPPContext lctx = { env := info.env, mctx := info.mctx, lctx := lctx, opts := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls }

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

Equations

• info.ppSyntax lctx stx = liftM (Lean.ppTerm (info.toPPContext lctx) { raw := stx })

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

Equations

• info.runMetaM ctx x = ctx.runMetaM info.lctx x

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

Equations

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

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

Equations

• Lean.Elab.PartialTermInfo.format ctx info = Std.format "Partial term @ " ++ Std.format (Lean.Elab.formatElabInfo✝ ctx info.toElabInfo) ++ Std.format ""

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

Equations

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

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

Equations

• Lean.Elab.CommandInfo.format ctx info = pure (Std.format "command @ " ++ Std.format (Lean.Elab.formatElabInfo✝ ctx info.toElabInfo) ++ Std.format "")

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• info.format = Std.format "UserWidget " ++ Std.format info.id ++ Std.format "\n" ++ Std.format (Std.format (StateT.run' info.props { })) ++ Std.format ""

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

Equations

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

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

Equations

• Lean.Elab.FieldRedeclInfo.format ctx info = Std.format "FieldRedecl @ " ++ Std.format (Lean.Elab.formatStxRange✝ ctx info.stx) ++ Std.format ""

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

Equations

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

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

Equations

• Lean.Elab.ChoiceInfo.format ctx info = Std.format "Choice @ " ++ Std.format (Lean.Elab.formatElabInfo✝ ctx info.toElabInfo) ++ Std.format ""

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

Equations

• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofTacticInfo i) = Lean.Elab.TacticInfo.format ctx i
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofTermInfo i) = Lean.Elab.TermInfo.format ctx i
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofPartialTermInfo i) = pure (Lean.Elab.PartialTermInfo.format ctx i)
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofCommandInfo i) = Lean.Elab.CommandInfo.format ctx i
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofMacroExpansionInfo i) = Lean.Elab.MacroExpansionInfo.format ctx i
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofOptionInfo i) = Lean.Elab.OptionInfo.format ctx i
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofFieldInfo i) = Lean.Elab.FieldInfo.format ctx i
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofCompletionInfo i) = Lean.Elab.CompletionInfo.format ctx i
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofUserWidgetInfo i) = pure i.format
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofCustomInfo i) = pure (Std.format i)
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofFVarAliasInfo i) = pure i.format
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofFieldRedeclInfo i) = pure (Lean.Elab.FieldRedeclInfo.format ctx i)
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofDelabTermInfo i) = Lean.Elab.DelabTermInfo.format ctx i
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofChoiceInfo i) = pure (Lean.Elab.ChoiceInfo.format ctx i)

def Lean.Elab.Info.toElabInfo? : Info → Option ElabInfo

Equations

• (Lean.Elab.Info.ofTacticInfo i).toElabInfo? = some i.toElabInfo
• (Lean.Elab.Info.ofTermInfo i).toElabInfo? = some i.toElabInfo
• (Lean.Elab.Info.ofPartialTermInfo i).toElabInfo? = some i.toElabInfo
• (Lean.Elab.Info.ofCommandInfo i).toElabInfo? = some i.toElabInfo
• (Lean.Elab.Info.ofMacroExpansionInfo i).toElabInfo? = none
• (Lean.Elab.Info.ofOptionInfo i).toElabInfo? = none
• (Lean.Elab.Info.ofFieldInfo i).toElabInfo? = none
• (Lean.Elab.Info.ofCompletionInfo i).toElabInfo? = none
• (Lean.Elab.Info.ofUserWidgetInfo i).toElabInfo? = none
• (Lean.Elab.Info.ofCustomInfo i).toElabInfo? = none
• (Lean.Elab.Info.ofFVarAliasInfo i).toElabInfo? = none
• (Lean.Elab.Info.ofFieldRedeclInfo i).toElabInfo? = none
• (Lean.Elab.Info.ofDelabTermInfo i).toElabInfo? = some i.toElabInfo
• (Lean.Elab.Info.ofChoiceInfo i).toElabInfo? = some i.toElabInfo

def Lean.Elab.Info.updateContext? : Option ContextInfo → Info → Option ContextInfo

Helper function for propagating the tactic metavariable context to its children nodes. We need this function because we preserve TacticInfo nodes during backtracking and their children. Moreover, we backtrack the metavariable context to undo metavariable assignments. TacticInfo nodes save the metavariable context before/after the tactic application, and can be pretty printed without any extra information. This is not the case for TermInfo nodes. Without this function, the formatting method would often fail when processing TermInfo nodes that are children of TacticInfo nodes that have been preserved during backtracking. Saving the metavariable context at TermInfo nodes is also not a good option because at TermInfo creation time, the metavariable context often miss information, e.g., a TC problem has not been resolved, a postponed subterm has not been elaborated, etc.

See Term.SavedState.restore.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Info.updateContext? x✝¹ x✝ = x✝¹

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.

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.pushInfoLeaf t = do let __do_lift ← Lean.Elab.getInfoState if __do_lift.enabled = true then Lean.Elab.pushInfoTree (Lean.Elab.InfoTree.node t { }) else pure PUnit.unit

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

Equations

• Lean.Elab.addCompletionInfo info = Lean.Elab.pushInfoLeaf (Lean.Elab.Info.ofCompletionInfo info)

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

Equations

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

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 sourcefile you will see the fully resolved name in the hover info.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

• Lean.Elab.getInfoHoleIdAssignment? mvarId = do let __do_lift ← Lean.Elab.getInfoState pure __do_lift.assignment[mvarId]

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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

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

Equations

• Lean.Elab.enableInfoTree flag = Lean.Elab.modifyInfoState fun (s : Lean.Elab.InfoState) => { enabled := flag, assignment := s.assignment, lazyAssignment := s.lazyAssignment, trees := s.trees }

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

Equations

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

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

Equations

• Lean.Elab.getInfoTrees = do let __do_lift ← Lean.Elab.getInfoState pure __do_lift.trees