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

Visit nodes, passing in a surrounding context (the innermost one) and accumulating results on the way back up.

Equations

• Lean.Elab.InfoTree.visitM preNode postNode = Lean.Elab.InfoTree.visitM.go preNode postNode none

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

def Lean.Elab.InfoTree.visitM' {m : Type → Type u_1} [inst : Monad m] (preNode : optParam (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m Unit) fun x x x => pure ()) (postNode : optParam (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m Unit) fun x x x => pure ()) (t : Lean.Elab.InfoTree) : m Unit

InfoTree.visitM specialized to Unit return type

Equations

• Lean.Elab.InfoTree.visitM' preNode postNode t = discard (Lean.Elab.InfoTree.visitM preNode (fun ci i cs x => postNode ci i cs) t)

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

• Lean.Elab.InfoTree.collectNodesBottomUp p i = Option.getD (Lean.Elab.InfoTree.visitM (fun x x x => pure ()) (fun ci i cs as => p ci i cs (List.join (List.filterMap id as))) i) []

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.Info.isTerm : Lean.Elab.Info → Bool

Equations

• Lean.Elab.Info.isTerm _fun_discr = match _fun_discr with | Lean.Elab.Info.ofTermInfo i => true | x => false

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

Equations

• Lean.Elab.Info.isCompletion _fun_discr = match _fun_discr with | Lean.Elab.Info.ofCompletionInfo i => true | x => 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

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

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

Equations

• Lean.Elab.Info.lctx _fun_discr = match _fun_discr with | Lean.Elab.Info.ofTermInfo i => i.lctx | Lean.Elab.Info.ofFieldInfo i => i.lctx | x => Lean.LocalContext.empty

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

Equations

• Lean.Elab.Info.pos? i = Lean.Syntax.getPos? (Lean.Elab.Info.stx i) true

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

Equations

• Lean.Elab.Info.tailPos? i = Lean.Syntax.getTailPos? (Lean.Elab.Info.stx i) true

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

Equations

• Lean.Elab.Info.range? i = Lean.Syntax.getRange? (Lean.Elab.Info.stx i) true

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

Equations

• Lean.Elab.Info.contains i pos includeStop = Option.any (fun a => String.Range.contains a pos includeStop) (Lean.Elab.Info.range? i)

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.Info.occursBefore? i hoverPos = do let tailPos ← Lean.Elab.Info.tailPos? i guard (tailPos ≤ hoverPos) pure (hoverPos - tailPos)

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

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 : optParam Bool false) (omitAppFns : optParam Bool false) : Option (Lean.Elab.ContextInfo × Lean.Elab.Info)

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

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

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

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.Format × Option Lean.Format)

Equations

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

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 (Lean.Format.group f 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 _fun_discr = false

structure Lean.Elab.GoalsAtResult : Type

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

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

  indented : Bool
• 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 : String.Pos) (pos : String.Pos) (tailPos : String.Pos) : Lean.Elab.InfoTree → Bool

def Lean.Elab.InfoTree.termGoalAt? (t : Lean.Elab.InfoTree) (hoverPos : String.Pos) : Option (Lean.Elab.ContextInfo × Lean.Elab.Info)

Equations

• Lean.Elab.InfoTree.termGoalAt? t hoverPos = Lean.Elab.InfoTree.hoverableInfoAt? t 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