Documentation

Lean.Namespace

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

Register a new namespace in the environment.

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

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

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

      Returns an iterator over all namespaces in env.

      Instances For