(vl-module-impexp-names x) → (mv implicit explicit)
Function:
(defun vl-module-impexp-names (x) (declare (xargs :guard (vl-module-p x))) (let ((__function__ 'vl-module-impexp-names)) (declare (ignorable __function__)) (vl-vardecllist-impexp-names (vl-module->vardecls x) nil nil)))
Theorem:
(defthm string-listp-of-vl-module-impexp-names.implicit (implies (and (force (vl-module-p x))) (b* (((mv ?implicit ?explicit) (vl-module-impexp-names x))) (string-listp implicit))) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-vl-module-impexp-names.explicit (implies (and (force (vl-module-p x))) (b* (((mv ?implicit ?explicit) (vl-module-impexp-names x))) (string-listp explicit))) :rule-classes :rewrite)