Documentation

Lean.Server.Completion

opaque Lean.Server.Completion.completionBlackListExt:

Lean.TagDeclarationExtension

@[export lean_completion_add_to_black_list]

def Lean.Server.Completion.addToBlackList (env : Lean.Environment) (declName : Lean.Name) :

Lean.Environment

Equations

Lean.Server.Completion.addToBlackList env declName = Lean.TagDeclarationExtension.tag Lean.Server.Completion.completionBlackListExt env declName

structure Lean.Server.Completion.State:

Type

itemsMain : Array (Lean.Lsp.CompletionItem × Float)
itemsOther : Array (Lean.Lsp.CompletionItem × Float)

@[inline]

abbrev Lean.Server.Completion.M (α : Type) :

Type

Equations

Lean.Server.Completion.M = OptionT (StateRefT' IO.RealWorld Lean.Server.Completion.State Lean.MetaM)

inductive Lean.Server.Completion.HoverInfo:

Type

after: Lean.Server.Completion.HoverInfo
inside: Nat → Lean.Server.Completion.HoverInfo

def Lean.Server.Completion.matchNamespace (ns : Lean.Name) (nsFragment : Lean.Name) (danglingDot : Bool) :

Equations

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

def Lean.Server.Completion.completeNamespaces (ctx : Lean.Elab.ContextInfo) (id : Lean.Name) (danglingDot : Bool) :

Lean.Server.Completion.M Unit

Equations

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

def Lean.Server.Completion.completeNamespaces.visitNamespaces (id : Lean.Name) (danglingDot : Bool) (add : Lean.Name → Lean.Name → Float → Lean.Server.Completion.M Unit) (ns : Lean.Name) (ns' : Lean.Name) :

Lean.Server.Completion.M Unit

Equations

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

def Lean.Server.Completion.find? (fileMap : Lean.FileMap) (hoverPos : String.Pos) (infoTree : Lean.Elab.InfoTree) (caps : Lean.Lsp.ClientCapabilities) :

IO (Option Lean.Lsp.CompletionList)

Equations

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

def Lean.Server.Completion.find?.choose (hoverPos : String.Pos) (fileMap : Lean.FileMap) (hoverLine : Nat) (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.Info) (best? : Option (Lean.Server.Completion.HoverInfo × Lean.Elab.ContextInfo × Lean.Elab.Info)) :

Option (Lean.Server.Completion.HoverInfo × Lean.Elab.ContextInfo × Lean.Elab.Info)

Equations

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