		Search-engine friendly clone of the ACL2 documentation.

Vl-namefactory-p

Vl-free-namefactory

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

Signature
(vl-free-namefactory factory) → *
Arguments: factory — Guard (vl-namefactory-p factory).

The name factory 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-namefactory

(defun vl-free-namefactory (factory)
  (declare (xargs :guard (vl-namefactory-p factory)))
  (let ((__function__ 'vl-free-namefactory))
    (declare (ignorable __function__))
    (progn$ (vl-free-namedb (vl-namefactory->namedb factory))
            nil)))