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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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