@[reducible, inline]

abbrev Lean.Server.Completion.EligibleHeaderDecls : Type

Equations

• Lean.Server.Completion.EligibleHeaderDecls = Std.HashMap Lean.Name Lean.ConstantInfo

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

Cached header declarations for which allowCompletion headerEnv decl is true.

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

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

Equations

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

def Lean.Server.Completion.forEligibleDeclsM {m : Type → Type} [Monad m] [Lean.MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT IO m] (f : Lean.Name → Lean.ConstantInfo → m PUnit) : m PUnit

Iterate over all declarations that are allowed in completion results.

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

Checks whether this declaration can appear in completion results.