		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-table-num-scopes

Number of scopes in a validation table.

Signature
(valid-table-num-scopes table) → num
Arguments: table — Guard (valid-tablep table).
Returns: num — Type (natp num).

Definitions and Theorems

Function: valid-table-num-scopes

(defun valid-table-num-scopes (table)
  (declare (xargs :guard (valid-tablep table)))
  (let ((__function__ 'valid-table-num-scopes))
    (declare (ignorable __function__))
    (len (valid-table->scopes table))))

Theorem: natp-of-valid-table-num-scopes

(defthm natp-of-valid-table-num-scopes
  (b* ((num (valid-table-num-scopes table)))
    (natp num))
  :rule-classes :rewrite)

Theorem: valid-table-num-scopes-of-valid-table-fix-table

(defthm valid-table-num-scopes-of-valid-table-fix-table
  (equal (valid-table-num-scopes (valid-table-fix table))
         (valid-table-num-scopes table)))

Theorem: valid-table-num-scopes-valid-table-equiv-congruence-on-table

(defthm valid-table-num-scopes-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-table-num-scopes table)
                  (valid-table-num-scopes table-equiv)))
  :rule-classes :congruence)