		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-namedb-allnames

(vl-namedb-p x) returns a list of all names that are considered to be used by the name db.

Signature
(vl-namedb-allnames db) → allnames
Arguments: db — Guard (vl-namedb-p db).
Returns: allnames — Type (string-listp allnames).

This function is not particularly efficient, and probably should not ordinarily be executed in real programs. Its main purpose is to establish the freshness guarantee for name DBs, described in vl-namedb-p.

Definitions and Theorems

Function: vl-namedb-allnames

(defun vl-namedb-allnames (db)
  (declare (xargs :guard (vl-namedb-p db)))
  (let ((__function__ 'vl-namedb-allnames))
    (declare (ignorable __function__))
    (alist-keys (vl-namedb->names db))))

Theorem: string-listp-of-vl-namedb-allnames

(defthm string-listp-of-vl-namedb-allnames
  (b* ((allnames (vl-namedb-allnames db)))
    (string-listp allnames))
  :rule-classes :rewrite)

Theorem: vl-namedb-allnames-of-vl-namedb-fix-db

(defthm vl-namedb-allnames-of-vl-namedb-fix-db
  (equal (vl-namedb-allnames (vl-namedb-fix db))
         (vl-namedb-allnames db)))

Theorem: vl-namedb-allnames-vl-namedb-equiv-congruence-on-db

(defthm vl-namedb-allnames-vl-namedb-equiv-congruence-on-db
  (implies (vl-namedb-equiv db db-equiv)
           (equal (vl-namedb-allnames db)
                  (vl-namedb-allnames db-equiv)))
  :rule-classes :congruence)