		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-init-table

Initial validation table.

Signature
(valid-init-table) → table
Returns: table — Type (valid-tablep table).

This contains one empty scope (the initial file scope).

Definitions and Theorems

Function: valid-init-table

(defun valid-init-table nil
  (declare (xargs :guard t))
  (let ((__function__ 'valid-init-table))
    (declare (ignorable __function__))
    (make-valid-table :scopes (list (valid-empty-scope)))))

Theorem: valid-tablep-of-valid-init-table

(defthm valid-tablep-of-valid-init-table
  (b* ((table (valid-init-table)))
    (valid-tablep table))
  :rule-classes :rewrite)