		Search-engine friendly clone of the ACL2 documentation.

Vl-namefactory-p

Vl-empty-namefactory

(vl-empty-namefactory) creates an empty name factory without a module.

Signature
(vl-empty-namefactory) → nf
Returns: nf — Type (vl-namefactory-p nf).

Usually you should use vl-starting-namefactory instead; vl-starting-namefactory automatically regards all of the names in the module as used, whereas vl-empty-namefactory regards no names as used.

On the other hand, vl-empty-namefactory may be useful when you are generating modules from scratch and, hence, don't have a module to give to vl-starting-namefactory yet.

Definitions and Theorems

Function: vl-empty-namefactory

(defun vl-empty-namefactory nil
  (declare (xargs :guard t))
  (let ((__function__ 'vl-empty-namefactory))
    (declare (ignorable __function__))
    (make-vl-namefactory :mod nil
                         :namedb (vl-empty-namedb))))

Theorem: vl-namefactory-p-of-vl-empty-namefactory

(defthm vl-namefactory-p-of-vl-empty-namefactory
  (b* ((nf (vl-empty-namefactory)))
    (vl-namefactory-p nf))
  :rule-classes :rewrite)

Theorem: vl-namefactory-allnames-of-vl-empty-namefactory

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