(vl-datatype->svex-modname x) → name
Function:
(defun vl-datatype->svex-modname (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-datatype->svex-modname)) (declare (ignorable __function__)) (hons-copy (sv::modname-fix (vl-datatype-fix x)))))
Theorem:
(defthm modname-p-of-vl-datatype->svex-modname (b* ((name (vl-datatype->svex-modname x))) (sv::modname-p name)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype->svex-modname-of-vl-datatype-fix-x (equal (vl-datatype->svex-modname (vl-datatype-fix x)) (vl-datatype->svex-modname x)))
Theorem:
(defthm vl-datatype->svex-modname-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype->svex-modname x) (vl-datatype->svex-modname x-equiv))) :rule-classes :congruence)