		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-empty-scope

Empty validator scope.

Signature
(valid-empty-scope) → scope
Returns: scope — Type (valid-scopep scope).

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

Definitions and Theorems

Function: valid-empty-scope

(defun valid-empty-scope nil
  (declare (xargs :guard t))
  (let ((__function__ 'valid-empty-scope))
    (declare (ignorable __function__))
    (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)