def String.charactersIn (a b : String) : Bool

partial def String.charactersIn.go (a b : String) (aPos bPos : Pos) : Bool

inductive Lean.Server.Completion.HoverInfo : Type

• after : HoverInfo
• inside (delta : Nat) : HoverInfo

structure Lean.Server.Completion.ContextualizedCompletionInfo : Type

• hoverInfo : HoverInfo
• ctx : Elab.ContextInfo
• info : Elab.CompletionInfo

def Lean.Server.Completion.minimizeGlobalIdentifierInContext (currNamespace : Name) (openDecls : List OpenDecl) (id : Name) : Name

partial def Lean.Server.Completion.minimizeGlobalIdentifierInContext.shortenIn (id contextNamespace : Name) : Name

def Lean.Server.Completion.unfoldDefinitionGuarded? (e : Expr) : MetaM (Option Expr)

def Lean.Server.Completion.getDotCompletionTypeNames (type : Expr) : MetaM (Array Name)

partial def Lean.Server.Completion.getDotCompletionTypeNames.visit (type : Expr) : StateRefT' IO.RealWorld (Array Name) MetaM Unit