		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Var-table-init

Create an initial variable table.

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

This contains a single (file) scope with no variables.

Definitions and Theorems

Function: var-table-init

(defun var-table-init nil
  (declare (xargs :guard t))
  (let ((__function__ 'var-table-init))
    (declare (ignorable __function__))
    (list nil)))

Theorem: var-tablep-of-var-table-init

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