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.

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

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

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

Return a set containing all namespaces in env.