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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.CustomInfo.format x = let i := x; Std.format "CustomInfo(" ++ Std.format (Dynamic.typeName i.value) ++ Std.format ")"

instance Lean.Elab.instToFormatCustomInfo : Lean.ToFormat Lean.Elab.CustomInfo

Equations

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

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.TermInfo.runMetaM info ctx x = Lean.Elab.ContextInfo.runMetaM ctx info.lctx x

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

Equations

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

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

Equations

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

def Lean.Elab.CommandInfo.format (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.CommandInfo) : IO Lean.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 : Lean.Elab.ContextInfo) (info : Lean.Elab.OptionInfo) : IO Lean.Format

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.UserWidgetInfo.format info = Std.format "UserWidget " ++ Std.format info.widgetId ++ Std.format "\n" ++ Std.format (Std.format info.props) ++ Std.format ""

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

Equations

• Lean.Elab.FVarAliasInfo.format info = Std.format "FVarAlias " ++ Std.format (Lean.Name.eraseMacroScopes info.userName) ++ Std.format ""

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Info.updateContext? : Option Lean.Elab.ContextInfo → Lean.Elab.Info → Option Lean.Elab.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.

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

def Lean.Elab.getResetInfoTrees {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] : m (Lean.PersistentArray Lean.Elab.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} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (t : Lean.Elab.InfoTree) : m Unit

Equations

• Lean.Elab.pushInfoTree t = do let __do_lift ← Lean.Elab.getInfoState if __do_lift.enabled = true then Lean.Elab.modifyInfoTrees fun ts => Lean.PersistentArray.push ts t else pure PUnit.unit

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.resolveGlobalConstNoOverloadWithInfo {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (id : Lean.Syntax) (expectedType? : optParam (Option Lean.Expr) none) : m Lean.Name

This does the same job as resolveGlobalConstNoOverload; 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.resolveGlobalConstWithInfos {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (id : Lean.Syntax) (expectedType? : optParam (Option Lean.Expr) none) : m (List Lean.Name)

Similar to resolveGlobalConstNoOverloadWithInfo, 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.resolveGlobalNameWithInfos {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (ref : Lean.Syntax) (id : Lean.Name) : m (List (Lean.Name × List String))

Similar to resolveGlobalName, 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} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] {α : Type} [inst : MonadFinally m] (x : m α) (mkInfo : α → m (Lean.Elab.Info ⊕ Lean.MVarId)) : m α

Use this to descend a node on the infotree that is being built.

It saves the current list of trees t₀ and resets it and then runs x >>= mkInfo, producing either an i : Info or a hole id. Running x >>= mkInfo will modify the trees state and produce a new list of trees t₁. In the i : Info case, t₁ become the children of a node node i t₁ that is appended to t₀.

Equations

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

def Lean.Elab.withInfoTreeContext {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] {α : Type} [inst : MonadFinally m] (x : m α) (mkInfoTree : Lean.PersistentArray Lean.Elab.InfoTree → m Lean.Elab.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} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] {α : Type} [inst : MonadFinally m] (x : m α) (mkInfo : m Lean.Elab.Info) : m α

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

Equations

• Lean.Elab.withInfoContext x mkInfo = Lean.Elab.withInfoTreeContext x fun trees => do let __do_lift ← mkInfo pure (Lean.Elab.InfoTree.node __do_lift trees)

def Lean.Elab.withSaveInfoContext {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] {α : Type} [inst : Lean.MonadNameGenerator m] [inst : MonadFinally m] [inst : Lean.MonadEnv m] [inst : Lean.MonadOptions m] [inst : Lean.MonadMCtx m] [inst : Lean.MonadResolveName m] [inst : Lean.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 Γ <$> 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.getInfoHoleIdAssignment? {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (mvarId : Lean.MVarId) : m (Option Lean.Elab.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} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (mvarId : Lean.MVarId) (infoTree : Lean.Elab.InfoTree) : m Unit

Equations

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

def Lean.Elab.withMacroExpansionInfo {m : Type → Type} {α : Type} [inst : MonadFinally m] [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] [inst : Lean.MonadLCtx m] (stx : Lean.Syntax) (output : Lean.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} [inst : MonadFinally m] [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] (mvarId : Lean.MVarId) (x : m α) : m α

Equations

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

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

Equations

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

def Lean.Elab.withEnableInfoTree {m : Type → Type} {α : Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] [inst : 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} [inst : Lean.Elab.MonadInfoTree m] [inst : Monad m] : m (Lean.PersistentArray Lean.Elab.InfoTree)

Equations

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