structure Lean.Server.Completion.EligibleDecl : Type

• info : ConstantInfo
• kind : MetaM Lsp.CompletionItemKind
• tags : MetaM (Array Lsp.CompletionItemTag)

@[reducible, inline]

abbrev Lean.Server.Completion.EligibleHeaderDecls : Type

opaque Lean.Server.Completion.eligibleHeaderDeclsMutex : Std.Mutex (Option EligibleHeaderDecls)

Cached header declarations for which allowCompletion headerEnv decl is true.

def Lean.Server.Completion.getCompletionKindForDecl (constInfo : ConstantInfo) : MetaM Lsp.CompletionItemKind

def Lean.Server.Completion.getCompletionTagsForDecl (declName : Name) : MetaM (Array Lsp.CompletionItemTag)

def Lean.Server.Completion.getEligibleHeaderDecls (env : Environment) : MetaM EligibleHeaderDecls

Returns the declarations in the header for which allowCompletion env decl is true, caching them if not already cached.

def Lean.Server.Completion.forEligibleDeclsM {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT MetaM m] (f : Name → EligibleDecl → m PUnit) : m PUnit

Iterate over all declarations that are allowed in completion results.

def Lean.Server.Completion.allowCompletion (eligibleHeaderDecls : EligibleHeaderDecls) (env : Environment) (declName : Name) : Bool

Checks whether this declaration can appear in completion results.