		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-empty-namedb

(vl-empty-namedb) creates an empty name db.

Signature
(vl-empty-namedb) → db
Returns: db — Type (vl-namedb-p db).

Definitions and Theorems

Function: vl-empty-namedb

(defun vl-empty-namedb nil
  (declare (xargs :guard t))
  (let ((__function__ 'vl-empty-namedb))
    (declare (ignorable __function__))
    (make-vl-namedb :names nil
                    :pmap nil
                    :pset nil)))

Theorem: vl-namedb-p-of-vl-empty-namedb

(defthm vl-namedb-p-of-vl-empty-namedb
  (b* ((db (vl-empty-namedb)))
    (vl-namedb-p db))
  :rule-classes :rewrite)

Theorem: vl-namedb-allnames-of-vl-empty-namedb

(defthm vl-namedb-allnames-of-vl-empty-namedb
  (equal (vl-namedb-allnames (vl-empty-namedb))
         nil))