structure Lean.Elab.InfoWithCtx : Type

Elaborator information with elaborator context.

It can be thought of as a "thunked" elaboration computation that allows us to retroactively extract type information, symbol locations, etc. through arbitrary invocations of runMetaM (where the necessary context and state can be reconstructed from ctx and info.lctx).

W.r.t. widgets, this is used to tag different parts of expressions in ppExprTagged. This is the input to the RPC call Lean.Widget.InteractiveDiagnostics.infoToInteractive. It carries over information about delaborated Info nodes in a CodeWithInfos, and the associated pretty-printing functionality is purpose-specific to showing the contents of infoview popups.

For use in standard LSP go-to-definition (see Lean.Server.FileWorker.locationLinksOfInfo), all the elaborator information we need for similar tasks is already fully recoverable via the InfoTree structure (see Lean.Elab.InfoTree.visitM). There we use this as a convenience wrapper for queried nodes (e.g. the return value of Lean.Elab.InfoTree.hoverableInfoAt?). It also includes the children info nodes as additional context (this is unused in the RPC case, as delaboration has no notion of child nodes).

NOTE: This type is for internal use in the infoview/LSP. It should not be used in user widgets.

• ctx : Lean.Elab.ContextInfo
• info : Lean.Elab.Info
• children : Lean.PersistentArray Lean.Elab.InfoTree

def Lean.Elab.InfoTree.visitM {m : Type → Type u_1} {α : Type} [Monad m] (preNode : Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m Bool := fun (x : Lean.Elab.ContextInfo) (x : Lean.Elab.Info) (x : Lean.PersistentArray Lean.Elab.InfoTree) => pure true) (postNode : Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List (Option α) → m α) (ctx? : Option Lean.Elab.ContextInfo := none) : Lean.Elab.InfoTree → m (Option α)

Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones) and accumulating results on the way back up. If preNode returns false, the children of the current node are skipped and postNode is invoked with an empty list of results.

Equations

• Lean.Elab.InfoTree.visitM preNode postNode ctx? = Lean.Elab.InfoTree.visitM.go preNode postNode ctx?

partial def Lean.Elab.InfoTree.visitM.go {m : Type → Type u_1} {α : Type} [Monad m] (preNode : Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m Bool := fun (x : Lean.Elab.ContextInfo) (x : Lean.Elab.Info) (x : Lean.PersistentArray Lean.Elab.InfoTree) => pure true) (postNode : Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List (Option α) → m α) : optParam (Option Lean.Elab.ContextInfo) none → Lean.Elab.InfoTree → m (Option α)

def Lean.Elab.InfoTree.visitM' {m : Type → Type u_1} [Monad m] (preNode : Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m Bool := fun (x : Lean.Elab.ContextInfo) (x : Lean.Elab.Info) (x : Lean.PersistentArray Lean.Elab.InfoTree) => pure true) (postNode : Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m Unit := fun (x : Lean.Elab.ContextInfo) (x : Lean.Elab.Info) (x : Lean.PersistentArray Lean.Elab.InfoTree) => pure ()) (ctx? : Option Lean.Elab.ContextInfo := none) (t : Lean.Elab.InfoTree) : m Unit

InfoTree.visitM specialized to Unit return type

Equations

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

def Lean.Elab.InfoTree.collectNodesBottomUp {α : Type} (p : Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List α → List α) (i : Lean.Elab.InfoTree) : List α

Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves).

Equations

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

def Lean.Elab.InfoTree.deepestNodes {α : Type} (p : Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → Option α) (infoTree : Lean.Elab.InfoTree) : List α

For every branch of the InfoTree, find the deepest node in that branch for which p returns some _ and return the union of all such nodes. The visitor p is given a node together with its innermost surrounding ContextInfo.

Equations

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

def Lean.Elab.InfoTree.foldInfo {α : Type u_1} (f : Lean.Elab.ContextInfo → Lean.Elab.Info → α → α) (init : α) : Lean.Elab.InfoTree → α

Equations

• Lean.Elab.InfoTree.foldInfo f init = Lean.Elab.InfoTree.foldInfo.go f none init

partial def Lean.Elab.InfoTree.foldInfo.go {α : Type u_1} (f : Lean.Elab.ContextInfo → Lean.Elab.Info → α → α) (ctx? : Option Lean.Elab.ContextInfo) (a : α) : Lean.Elab.InfoTree → α

def Lean.Elab.InfoTree.foldInfoTree {α : Type u_1} (init : α) (f : Lean.Elab.ContextInfo → Lean.Elab.InfoTree → α → α) : Lean.Elab.InfoTree → α

Fold an info tree as follows, while ensuring that the correct ContextInfo is supplied at each stage:

• Nodes are combined with the initial value init using f, and the result is then combined with the children using a left fold
• On InfoTree holes, we just return the initial value.

This is like InfoTree.foldInfo, but it also passes the whole node to f instead of just the head.

Equations

• Lean.Elab.InfoTree.foldInfoTree init f = Lean.Elab.InfoTree.foldInfoTree.go f none init

partial def Lean.Elab.InfoTree.foldInfoTree.go {α : Type u_1} (f : Lean.Elab.ContextInfo → Lean.Elab.InfoTree → α → α) (ctx? : Option Lean.Elab.ContextInfo) (a : α) : Lean.Elab.InfoTree → α

foldInfoTree.go is like foldInfoTree but with an additional outer context parameter ctx?.

def Lean.Elab.Info.isTerm : Lean.Elab.Info → Bool

Equations

• (Lean.Elab.Info.ofTermInfo i).isTerm = true
• x.isTerm = false

def Lean.Elab.Info.isCompletion : Lean.Elab.Info → Bool

Equations

• (Lean.Elab.Info.ofCompletionInfo i).isCompletion = true
• x.isCompletion = false

def Lean.Elab.InfoTree.getCompletionInfos (infoTree : Lean.Elab.InfoTree) : Array (Lean.Elab.ContextInfo × Lean.Elab.CompletionInfo)

Equations

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

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

Equations

• (Lean.Elab.Info.ofTacticInfo i).stx = i.stx
• (Lean.Elab.Info.ofTermInfo i).stx = i.stx
• (Lean.Elab.Info.ofCommandInfo i).stx = i.stx
• (Lean.Elab.Info.ofMacroExpansionInfo i).stx = i.stx
• (Lean.Elab.Info.ofOptionInfo i).stx = i.stx
• (Lean.Elab.Info.ofFieldInfo i).stx = i.stx
• (Lean.Elab.Info.ofCompletionInfo i).stx = i.stx
• (Lean.Elab.Info.ofCustomInfo i).stx = i.stx
• (Lean.Elab.Info.ofUserWidgetInfo i).stx = i.stx
• (Lean.Elab.Info.ofFVarAliasInfo i).stx = Lean.Syntax.missing
• (Lean.Elab.Info.ofFieldRedeclInfo i).stx = i.stx
• (Lean.Elab.Info.ofOmissionInfo i).stx = i.stx

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

Equations

• (Lean.Elab.Info.ofTermInfo i).lctx = i.lctx
• (Lean.Elab.Info.ofFieldInfo i).lctx = i.lctx
• (Lean.Elab.Info.ofOmissionInfo i).lctx = i.lctx
• (Lean.Elab.Info.ofMacroExpansionInfo i).lctx = i.lctx
• (Lean.Elab.Info.ofCompletionInfo i).lctx = i.lctx
• x.lctx = Lean.LocalContext.empty

def Lean.Elab.Info.pos? (i : Lean.Elab.Info) : Option String.Pos

Equations

• i.pos? = i.stx.getPos? true

def Lean.Elab.Info.tailPos? (i : Lean.Elab.Info) : Option String.Pos

Equations

• i.tailPos? = i.stx.getTailPos? true

def Lean.Elab.Info.range? (i : Lean.Elab.Info) : Option String.Range

Equations

• i.range? = i.stx.getRange? true

def Lean.Elab.Info.contains (i : Lean.Elab.Info) (pos : String.Pos) (includeStop : Bool := false) : Bool

Equations

• i.contains pos includeStop = Option.any (fun (x : String.Range) => x.contains pos includeStop) i.range?

def Lean.Elab.Info.size? (i : Lean.Elab.Info) : Option String.Pos

Equations

• i.size? = do let pos ← i.pos? let tailPos ← i.tailPos? pure (tailPos - pos)

def Lean.Elab.Info.isSmaller (i₁ i₂ : Lean.Elab.Info) : Bool

Equations

• i₁.isSmaller i₂ = match i₁.size?, i₂.size? with | some sz₁, some sz₂ => decide (sz₁ < sz₂) | some val, none => true | x, x_1 => false

def Lean.Elab.Info.occursInside? (i : Lean.Elab.Info) (hoverPos : String.Pos) : Option String.Pos

Equations

• i.occursInside? hoverPos = do let headPos ← i.pos? let tailPos ← i.tailPos? guard ((decide (headPos ≤ hoverPos) && decide (hoverPos < tailPos)) = true) pure (hoverPos - headPos)

def Lean.Elab.Info.occursInOrOnBoundary (i : Lean.Elab.Info) (hoverPos : String.Pos) : Bool

Equations

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

def Lean.Elab.InfoTree.smallestInfo? (p : Lean.Elab.Info → Bool) (t : Lean.Elab.InfoTree) : Option (Lean.Elab.ContextInfo × Lean.Elab.Info)

Equations

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

def Lean.Elab.InfoTree.hoverableInfoAt? (t : Lean.Elab.InfoTree) (hoverPos : String.Pos) (includeStop omitAppFns omitIdentApps : Bool := false) : Option Lean.Elab.InfoWithCtx

Find an info node, if any, which should be shown on hover/cursor at position hoverPos.

Equations

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

def Lean.Elab.Info.type? (i : Lean.Elab.Info) : Lean.MetaM (Option Lean.Expr)

Equations

• (Lean.Elab.Info.ofTermInfo ti).type? = do let a ← Lean.Meta.inferType ti.expr pure (some a)
• (Lean.Elab.Info.ofFieldInfo fi).type? = do let a ← Lean.Meta.inferType fi.val pure (some a)
• (Lean.Elab.Info.ofOmissionInfo oi).type? = do let a ← Lean.Meta.inferType oi.expr pure (some a)
• i.type? = pure none

def Lean.Elab.Info.docString? (i : Lean.Elab.Info) : Lean.MetaM (Option String)

Equations

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

def Lean.Elab.Info.fmtHover? (ci : Lean.Elab.ContextInfo) (i : Lean.Elab.Info) : IO (Option Lean.FormatWithInfos)

Construct a hover popup, if any, from an info node in a context.

Equations

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

def Lean.Elab.Info.fmtHover?.fmtModule? (decl : Lean.Name) : Lean.MetaM (Option Lean.Format)

Equations

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

def Lean.Elab.Info.fmtHover?.fmtTermAndModule? (i : Lean.Elab.Info) : Lean.MetaM (Option Lean.FormatWithInfos × Option Lean.Format)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Info.fmtHover?.fmtTermAndModule? i = pure (none, none)

def Lean.Elab.Info.fmtHover?.isAtomicFormat : Lean.Format → Bool

Equations

• Lean.Elab.Info.fmtHover?.isAtomicFormat (Std.Format.text a) = true
• Lean.Elab.Info.fmtHover?.isAtomicFormat (f.group behavior) = Lean.Elab.Info.fmtHover?.isAtomicFormat f
• Lean.Elab.Info.fmtHover?.isAtomicFormat (Lean.Format.nest indent f) = Lean.Elab.Info.fmtHover?.isAtomicFormat f
• Lean.Elab.Info.fmtHover?.isAtomicFormat (Lean.Format.tag a f) = Lean.Elab.Info.fmtHover?.isAtomicFormat f
• Lean.Elab.Info.fmtHover?.isAtomicFormat x = false

structure Lean.Elab.GoalsAtResult : Type

• ctxInfo : Lean.Elab.ContextInfo
• tacticInfo : Lean.Elab.TacticInfo
• useAfter : Bool
• indented : Bool

  Whether the tactic info is further indented than the hover position.

• priority : Nat

def Lean.Elab.InfoTree.goalsAt? (text : Lean.FileMap) (t : Lean.Elab.InfoTree) (hoverPos : String.Pos) : List Lean.Elab.GoalsAtResult

Try to retrieve TacticInfo for hoverPos. We retrieve all TacticInfo nodes s.t. hoverPos is inside the node's range plus trailing whitespace. We usually prefer the innermost such nodes so that for composite tactics such as induction, we show the nested proofs' states. However, if hoverPos is after the tactic, we prefer nodes that are not indented relative to it, meaning that e.g. at | in

have := by
  exact foo
|

we show the (final, see below) state of have, not exact.

Moreover, we instruct the LSP server to use the state after tactic execution if

• the hover position is after the info's start position and
• there is no nested tactic info after the hover position (tactic combinators should decide for themselves where to show intermediate states by calling withTacticInfoContext)

Equations

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

partial def Lean.Elab.InfoTree.goalsAt?.hasNestedTactic (hoverPos pos tailPos : String.Pos) : Lean.Elab.InfoTree → Bool

def Lean.Elab.InfoTree.goalsAt?.isEmptyBy (stx : Lean.Syntax) : Bool

Equations

• Lean.Elab.InfoTree.goalsAt?.isEmptyBy stx = (stx.getNumArgs == 2 && Lean.Syntax.isToken "by" stx[0] && stx[1].getNumArgs == 1 && stx[1][0].isMissing)

def Lean.Elab.InfoTree.termGoalAt? (t : Lean.Elab.InfoTree) (hoverPos : String.Pos) : Option Lean.Elab.InfoWithCtx

Equations

• t.termGoalAt? hoverPos = t.hoverableInfoAt? hoverPos true true

def Lean.Elab.InfoTree.hasSorry : Lean.Elab.InfoTree → IO Bool

Equations

• Lean.Elab.InfoTree.hasSorry = Lean.Elab.InfoTree.hasSorry.go none

partial def Lean.Elab.InfoTree.hasSorry.go (ci? : Option Lean.Elab.ContextInfo) : Lean.Elab.InfoTree → IO Bool