Get the namedb field from a vl-namefactory.
(vl-namefactory->namedb x) → namedb
This is an ordinary field accessor created by defprod.
Function:
(defun vl-namefactory->namedb$inline (x) (declare (xargs :guard (vl-namefactory-p x))) (declare (xargs :guard t)) (let ((__function__ 'vl-namefactory->namedb)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and t x)) (mod (vl-maybe-module-fix (std::prod-car (cdr x)))) (namedb (vl-namedb-fix (std::prod-cdr (cdr x))))) (vl-namefactory-namedb-fix mod namedb)) :exec (std::prod-cdr (cdr x)))))
Theorem:
(defthm vl-namedb-p-of-vl-namefactory->namedb (b* ((namedb (vl-namefactory->namedb$inline x))) (vl-namedb-p namedb)) :rule-classes :rewrite)
Theorem:
(defthm vl-namefactory->namedb$inline-of-vl-namefactory-fix-x (equal (vl-namefactory->namedb$inline (vl-namefactory-fix x)) (vl-namefactory->namedb$inline x)))
Theorem:
(defthm vl-namefactory->namedb$inline-vl-namefactory-equiv-congruence-on-x (implies (vl-namefactory-equiv x x-equiv) (equal (vl-namefactory->namedb$inline x) (vl-namefactory->namedb$inline x-equiv))) :rule-classes :congruence)