		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-starting-namedb

(vl-starting-namedb names) creates a name database that regards names as already in use.

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

Definitions and Theorems

Function: vl-starting-namedb

(defun vl-starting-namedb (names)
 (declare (xargs :guard (string-listp names)))
 (let ((__function__ 'vl-starting-namedb))
  (declare (ignorable __function__))
  (make-vl-namedb :names (make-lookup-alist (string-list-fix names))
                  :pmap nil
                  :pset nil)))

Theorem: vl-namedb-p-of-vl-starting-namedb

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

Theorem: vl-namedb-allnames-of-vl-starting-namedb

(defthm vl-namedb-allnames-of-vl-starting-namedb
  (equal (vl-namedb-allnames (vl-starting-namedb names))
         (string-list-fix names)))

Theorem: vl-starting-namedb-of-string-list-fix-names

(defthm vl-starting-namedb-of-string-list-fix-names
  (equal (vl-starting-namedb (string-list-fix names))
         (vl-starting-namedb names)))

Theorem: vl-starting-namedb-string-list-equiv-congruence-on-names

(defthm vl-starting-namedb-string-list-equiv-congruence-on-names
  (implies (str::string-list-equiv names names-equiv)
           (equal (vl-starting-namedb names)
                  (vl-starting-namedb names-equiv)))
  :rule-classes :congruence)