opaque Lean.namespacesExt : SimplePersistentEnvExtension Name NameSSet

Environment extension for tracking all namespace declared by users.

def Lean.Environment.registerNamespace (env : Environment) (n : Name) : Environment

Register a new namespace in the environment.

Equations

• env.registerNamespace n = if (Lean.namespacesExt.getState env).contains n = true then env else Lean.PersistentEnvExtension.addEntry Lean.namespacesExt env n

def Lean.Environment.isNamespace (env : Environment) (n : Name) : Bool

Return true if n is the name of a namespace in env.

Equations

• env.isNamespace n = (Lean.namespacesExt.getState env).contains n

def Lean.Environment.getNamespaceSet (env : Environment) : NameSSet

Return a set containing all namespaces in env.

Equations

• env.getNamespaceSet = Lean.namespacesExt.getState env