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.CustomInfo.format : CustomInfo → Format

Equations

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

@[instance_reducible]

instance Lean.Elab.instToFormatCustomInfo : ToFormat CustomInfo

Equations

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

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 "[PartialTerm] @ " ++ Std.format (Lean.Elab.formatElabInfo✝ ctx info.toElabInfo)

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.CompletionInfo.format ctx info = pure (Std.format "[Completion] " ++ Std.format info.stx ++ Std.format " @ " ++ Std.format (Lean.Elab.formatStxRange✝ ctx info.stx))

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

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

Equations

• Lean.Elab.OptionInfo.format ctx info = pure (Std.format "[Option] " ++ Std.format info.optionName ++ Std.format " @ " ++ Std.format (Lean.Elab.formatStxRange✝ ctx info.stx))

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

Equations

• Lean.Elab.ErrorNameInfo.format ctx info = pure (Std.format "[ErrorName] " ++ Std.format info.errorName ++ Std.format " @ " ++ Std.format (Lean.Elab.formatStxRange✝ ctx info.stx))

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 { }))

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)

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

Equations

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

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)

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

Equations

• Lean.Elab.DocInfo.format ctx info = Std.format "[Doc] " ++ Std.format info.stx.getKind ++ Std.format " @ " ++ Std.format (Lean.Elab.formatElabInfo✝ ctx info.toElabInfo)

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

Equations

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

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.ofErrorNameInfo i) = Lean.Elab.ErrorNameInfo.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)
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofDocInfo i) = pure (Lean.Elab.DocInfo.format ctx i)
• Lean.Elab.Info.format ctx (Lean.Elab.Info.ofDocElabInfo i) = pure (Lean.Elab.DocElabInfo.format ctx i)

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

Equations

• (Lean.Elab.PartialContextInfo.commandCtx info).format = Std.Format.text "command"
• (Lean.Elab.PartialContextInfo.parentDeclCtx n).format = Std.Format.text (toString "parent[" ++ toString n ++ toString "]")
• (Lean.Elab.PartialContextInfo.autoImplicitCtx implicits).format = Std.Format.text (toString "autoImplicits[" ++ toString implicits ++ toString "]")

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 ()

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

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 α

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

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