@[reducible, inline]

abbrev Lean.Server.Completion.EligibleHeaderDecls : Type

opaque Lean.Server.Completion.eligibleHeaderDeclsRef : IO.Ref (Option EligibleHeaderDecls)

Cached header declarations for which allowCompletion headerEnv decl is true.

def Lean.Server.Completion.getEligibleHeaderDecls (env : Environment) : IO 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 (ST IO.RealWorld) m] [MonadLiftT IO m] (f : Name → ConstantInfo → 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.