Lean.Server.InfoUtils

source

structure String.Range:

Type

start : String.Pos
stop : String.Pos

source

instance String.instInhabitedRange:

Inhabited String.Range

Equations

String.instInhabitedRange = { default := { start := default, stop := default } }

source

instance String.instReprRange:

Repr String.Range

Equations

String.instReprRange = { reprPrec := [anonymous] }

source

instance String.instBEqRange:

BEq String.Range

Equations

String.instBEqRange = { beq := [anonymous] }

source

instance String.instHashableRange:

Hashable String.Range

Equations

String.instHashableRange = { hash := [anonymous] }

source

def String.Range.contains (r : String.Range) (pos : String.Pos) (includeStop : optParam Bool false) :

Bool

Equations

String.Range.contains r pos includeStop = (decide (r.start ≤ pos) && if includeStop = true then decide (pos ≤ r.stop) else decide (pos < r.stop))

source

def Lean.Syntax.getRange? (stx : Lean.Syntax) (originalOnly : optParam Bool false) :

Option String.Range

Equations

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

source

def Lean.Elab.InfoTree.visitM {m : Type → Type u_1} {α : Type} [inst : Monad m] [inst : Inhabited α] (preNode : optParam (Lean.Elab.ContextInfo → Lean.Elab.Info → Std.PersistentArray Lean.Elab.InfoTree → m Unit) fun x x x => pure ()) (postNode : Lean.Elab.ContextInfo → Lean.Elab.Info → Std.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

source

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

Option Lean.Elab.ContextInfo → Lean.Elab.InfoTree → m (Option α)

source

def Lean.Elab.InfoTree.collectNodesBottomUp {α : Type} (p : Lean.Elab.ContextInfo → Lean.Elab.Info → Std.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) []

source

def Lean.Elab.InfoTree.deepestNodes {α : Type} (p : Lean.Elab.ContextInfo → Lean.Elab.Info → Std.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.

source

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

source

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 → α

source

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

source

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

source

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.

source

def Lean.Elab.Info.stx:

Lean.Elab.Info → Lean.Syntax

Equations

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

source

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

source

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

source

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

source

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

source

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)

source

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)

source

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

Bool

Equations

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

source

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)

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

def Lean.Elab.Info.fmtHover?.fmtTerm? (i : Lean.Elab.Info) :

Lean.MetaM (Option Lean.Format)

Equations

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

source

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

source

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

List Lean.Elab.GoalsAtResult

Equations