def Lean.Server.Completion.idCompletion (mod : Name) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (stx : Syntax) (id : Name) (hoverInfo : HoverInfo) (danglingDot : Bool) : CancellableM (Array Lsp.ResolvableCompletionItem)

def Lean.Server.Completion.dotCompletion (mod : Name) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (info : Elab.TermInfo) : CancellableM (Array Lsp.ResolvableCompletionItem)

def Lean.Server.Completion.dotIdCompletion (mod : Name) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (id : Name) (expectedType? : Option Expr) : CancellableM (Array Lsp.ResolvableCompletionItem)

def Lean.Server.Completion.fieldIdCompletion (mod : Name) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (lctx : LocalContext) (id : Option Name) (structName : Name) : CancellableM (Array Lsp.ResolvableCompletionItem)

def Lean.Server.Completion.optionCompletion (mod : Name) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (stx : Syntax) (caps : Lsp.ClientCapabilities) : IO (Array Lsp.ResolvableCompletionItem)

def Lean.Server.Completion.errorNameCompletion (mod : Name) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) (partialId : Syntax) (caps : Lsp.ClientCapabilities) : IO (Array Lsp.ResolvableCompletionItem)

def Lean.Server.Completion.tacticCompletion (mod : Name) (pos : Lsp.Position) (completionInfoPos : Nat) (ctx : Elab.ContextInfo) : IO (Array Lsp.ResolvableCompletionItem)

def Lean.Server.Completion.endSectionCompletion (mod : Name) (pos : Lsp.Position) (completionInfoPos : Nat) (id? : Option Name) (danglingDot : Bool) (scopeNames : List String) : IO (Array Lsp.ResolvableCompletionItem)