		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-pop-scope

Pop a scope from the validation table.

Signature
(valid-pop-scope table) → new-table
Arguments: table — Guard (valid-tablep table).
Returns: new-table — Type (valid-tablep new-table).

The guard requires that there are is at least one scope.

The popped scope is discarded.

Definitions and Theorems

Function: valid-pop-scope

(defun valid-pop-scope (table)
  (declare (xargs :guard (valid-tablep table)))
  (let ((__function__ 'valid-pop-scope))
    (declare (ignorable __function__))
    (b* (((unless (> (valid-table-num-scopes table) 0))
          (raise "Internal error: no scopes in validation table.")
          (valid-table-fix table))
         (scopes (valid-table->scopes table))
         (new-scopes (cdr scopes)))
      (change-valid-table table
                          :scopes new-scopes))))

Theorem: valid-tablep-of-valid-pop-scope

(defthm valid-tablep-of-valid-pop-scope
  (b* ((new-table (valid-pop-scope table)))
    (valid-tablep new-table))
  :rule-classes :rewrite)

Theorem: valid-table-num-scopes-of-valid-pop-scope

(defthm valid-table-num-scopes-of-valid-pop-scope
  (implies (> (valid-table-num-scopes table) 0)
           (b* ((?new-table (valid-pop-scope table)))
             (equal (valid-table-num-scopes new-table)
                    (1- (valid-table-num-scopes table))))))

Theorem: valid-pop-scope-of-valid-table-fix-table

(defthm valid-pop-scope-of-valid-table-fix-table
  (equal (valid-pop-scope (valid-table-fix table))
         (valid-pop-scope table)))

Theorem: valid-pop-scope-valid-table-equiv-congruence-on-table

(defthm valid-pop-scope-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-pop-scope table)
                  (valid-pop-scope table-equiv)))
  :rule-classes :congruence)