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

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 true else false else false

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 → 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.
• Lean.Server.Completion.completeNamespaces.visitNamespaces id danglingDot add ns ns' = if Lean.Server.Completion.matchNamespace ns (ns' ++ id) danglingDot = true then add ns ns' else pure ()

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

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) : CancellableM (Array Lsp.CompletionItem)

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) : CancellableM (Array Lsp.CompletionItem)

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

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 Lsp.CompletionItem)

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 Lsp.CompletionItem)

Equations

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