		Search-engine friendly clone of the ACL2 documentation.

Vl-namefactory-p

Vl-starting-namefactory

(vl-starting-namefactory mod) creates a name factory for a module.

Signature
(vl-starting-namefactory mod) → nf
Arguments: mod — Guard (vl-module-p mod).
Returns: nf — Type (vl-namefactory-p nf).

This function is very cheap to call because the real work of initializing the name factory is deferred to its first use. See vl-namefactory-p for all name factory documentation.

Definitions and Theorems

Function: vl-starting-namefactory

(defun vl-starting-namefactory (mod)
  (declare (xargs :guard (vl-module-p mod)))
  (let ((__function__ 'vl-starting-namefactory))
    (declare (ignorable __function__))
    (make-vl-namefactory :mod (vl-module-fix mod)
                         :namedb (vl-empty-namedb))))

Theorem: vl-namefactory-p-of-vl-starting-namefactory

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

Theorem: vl-namefactory-allnames-of-vl-starting-namefactory

(defthm vl-namefactory-allnames-of-vl-starting-namefactory
  (equal (vl-namefactory-allnames (vl-starting-namefactory mod))
         (vl-module->modnamespace mod)))

Theorem: vl-starting-namefactory-of-vl-module-fix-mod

(defthm vl-starting-namefactory-of-vl-module-fix-mod
  (equal (vl-starting-namefactory (vl-module-fix mod))
         (vl-starting-namefactory mod)))

Theorem: vl-starting-namefactory-vl-module-equiv-congruence-on-mod

(defthm vl-starting-namefactory-vl-module-equiv-congruence-on-mod
  (implies (vl-module-equiv mod mod-equiv)
           (equal (vl-starting-namefactory mod)
                  (vl-starting-namefactory mod-equiv)))
  :rule-classes :congruence)