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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Server.Completion.dotCompletion
(mod : Name)
(pos : Lsp.Position)
(completionInfoPos : Nat)
(ctx : Elab.ContextInfo)
(info : Elab.TermInfo)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Server.Completion.dotIdCompletion
(mod : Name)
(pos : Lsp.Position)
(completionInfoPos : Nat)
(ctx : Elab.ContextInfo)
(lctx : LocalContext)
(id : Name)
(expectedType? : Option Expr)
:
Instances For
def
Lean.Server.Completion.fieldIdCompletion
(mod : Name)
(pos : Lsp.Position)
(completionInfoPos : Nat)
(ctx : Elab.ContextInfo)
(lctx : LocalContext)
(id : Option Name)
(structName : Name)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Server.Completion.optionCompletion
(mod : Name)
(pos : Lsp.Position)
(completionInfoPos : Nat)
(ctx : Elab.ContextInfo)
(stx : Syntax)
(caps : Lsp.ClientCapabilities)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Server.Completion.errorNameCompletion
(mod : Name)
(pos : Lsp.Position)
(completionInfoPos : Nat)
(ctx : Elab.ContextInfo)
(partialId : Syntax)
(caps : Lsp.ClientCapabilities)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Server.Completion.tacticCompletion
(mod : Name)
(pos : Lsp.Position)
(completionInfoPos : Nat)
(ctx : Elab.ContextInfo)
:
Equations
- One or more equations did not get rendered due to their size.