def Lean.Server.Completion.bestLabelForDecl? (ctx : Elab.ContextInfo) (declName id : Name) (danglingDot : Bool) : Lean.Server.Completion.M✝ (Option Name)

def Lean.Server.Completion.bestLabelForDecl?.visitNamespaces (matchUsingNamespace : Name → StateT (Option Name) Lean.Server.Completion.M✝ Unit) (ns : Name) : StateT (Option Name) Lean.Server.Completion.M✝ Unit

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

def Lean.Server.Completion.idCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (stx : Syntax) (id : Name) (hoverInfo : HoverInfo) (danglingDot : Bool) : CancellableM (Array Lsp.CompletionItem)

def Lean.Server.Completion.dotCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (info : Elab.TermInfo) : CancellableM (Array Lsp.CompletionItem)

def Lean.Server.Completion.dotIdCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (id : Name) (expectedType? : Option Expr) : CancellableM (Array Lsp.CompletionItem)

def Lean.Server.Completion.fieldIdCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (id : Option Name) (structName : Name) : CancellableM (Array Lsp.CompletionItem)

def Lean.Server.Completion.optionCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (stx : Syntax) (caps : Lsp.ClientCapabilities) : IO (Array Lsp.CompletionItem)

def Lean.Server.Completion.errorNameCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (partialId : Syntax) (caps : Lsp.ClientCapabilities) : IO (Array Lsp.CompletionItem)

def Lean.Server.Completion.tacticCompletion (params : Lsp.CompletionParams) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) : IO (Array Lsp.CompletionItem)