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

Register a new namespace in the environment.

Equations

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

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.SMap.contains (Lean.namespacesExt✝.getState env) n

def Lean.Environment.getNamespaces (env : Environment) : Std.Iter Name

Returns an iterator over all namespaces in env.

Equations

• env.getNamespaces = Std.Iter.map (fun (x : Lean.Name × Lean.Environment.Visibility) => x.fst) (Lean.SMap.iter (Lean.namespacesExt✝.getState env))