		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-free-namedb

(vl-free-namedb db) frees the fast alists associated with a name db and returns nil.

Signature
(vl-free-namedb db) → *
Arguments: db — Guard (vl-namedb-p db).

The name db should never be used after this function is called, since doing so will result in fast-alist discipline failures.

Note that we leave this function enabled.

Definitions and Theorems

Function: vl-free-namedb

(defun vl-free-namedb (db)
  (declare (xargs :guard (vl-namedb-p db)))
  (let ((__function__ 'vl-free-namedb))
    (declare (ignorable __function__))
    (progn$ (fast-alist-free (vl-namedb->names db))
            (fast-alist-free (vl-namedb->pmap db))
            (fast-alist-free (vl-namedb->pset db))
            nil)))