structure Lean.Server.Completion.ScoredCompletionItem : Type

• item : Lsp.CompletionItem
• score : Float

instance Lean.Server.Completion.instInhabitedScoredCompletionItem : Inhabited ScoredCompletionItem

Equations

• Lean.Server.Completion.instInhabitedScoredCompletionItem = { default := { item := default, score := default } }

def Lean.Server.Completion.matchNamespace (ns nsFragment : Name) (danglingDot : Bool) : Option Float

Equations

• One or more equations did not get rendered due to their size.
• Lean.Server.Completion.matchNamespace ns nsFragment danglingDot = if danglingDot = true then if (nsFragment != ns && nsFragment.isPrefixOf ns) = true then some 1 else none else none

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

Equations

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

def Lean.Server.Completion.completeNamespaces.visitNamespaces (id : Name) (danglingDot : Bool) (add : Name → Name → Float → Lean.Server.Completion.M✝ Unit) (ns ns' : Name) : Lean.Server.Completion.M✝ Unit

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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