		Search-engine friendly clone of the ACL2 documentation.

Valid-empty-scope

Empty validator scope.

Scopes always start empty, i.e. with no identifiers. This function returns the empty scope.

Function: valid-empty-scope

(defun valid-empty-scope nil
  (declare (xargs :guard t))
  (make-valid-scope :ord nil))

Theorem: valid-scopep-of-valid-empty-scope

(defthm valid-scopep-of-valid-empty-scope
  (b* ((scope (valid-empty-scope)))
    (valid-scopep scope))
  :rule-classes :rewrite)