source
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)
Equations

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

Instances For

source
def Lean.Server.Completion.dotCompletion (mod : Name) (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.

Instances For

source
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)
Instances For

source
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)
Equations

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

Instances For

source
def Lean.Server.Completion.optionCompletion (mod : Name) (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.

Instances For

source
def Lean.Server.Completion.errorNameCompletion (mod : Name) (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.

Instances For

source
def Lean.Server.Completion.tacticCompletion (mod : Name) (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.

Instances For

source
def Lean.Server.Completion.endSectionCompletion (mod : Name) (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.

Instances For