opaque Lean.Server.Completion.completionBlackListExt : Lean.TagDeclarationExtension

@[export lean_completion_add_to_black_list]

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

structure Lean.Server.Completion.State : Type

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

@[inline, reducible]

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

inductive Lean.Server.Completion.HoverInfo : Type

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

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

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

def Lean.Server.Completion.completeNamespaces.visitNamespaces (id : Lake.Name) (danglingDot : Bool) (add : Lake.Name → Lake.Name → Float → Lean.Server.Completion.M Unit) (ns : Lake.Name) (ns' : Lake.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)

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)