source
opaque Lean.namespacesExt :
SimplePersistentEnvExtension Name NameSSet

Environment extension for tracking all `namespace` declared by users.

source
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

Instances For

source
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

Instances For

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

Return a set containing all namespaces in `env`.

Equations

- env.getNamespaceSet = Lean.namespacesExt.getState env

Instances For