structure Lean.Server.Completion.ScoredCompletionItem : Type

• item : Lean.Lsp.CompletionItem
• score : Float

instance Lean.Server.Completion.instInhabitedScoredCompletionItem : Inhabited Lean.Server.Completion.ScoredCompletionItem

Equations

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

def Lean.Server.Completion.matchNamespace (ns nsFragment : Lean.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 : Lean.Elab.ContextInfo) (id : Lean.Name) (danglingDot : Bool) : Lean.Server.Completion.M✝ Unit

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

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

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

Equations

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

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

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

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

Equations

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

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

Equations

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