(vl-description->comments x) → comments
Function:
(defun vl-description->comments (x) (declare (xargs :guard (vl-description-p x))) (declare (xargs :guard (vl-description-has-comments-p x))) (let ((__function__ 'vl-description->comments)) (declare (ignorable __function__)) (b* ((x (vl-description-fix x))) (case (tag x) (:vl-module (vl-module->comments x)) (:vl-udp (vl-udp->comments x)) (:vl-interface (vl-interface->comments x)) (:vl-package (vl-package->comments x)) (:vl-program (vl-program->comments x)) (:vl-class (vl-class->comments x)) (:vl-config (vl-config->comments x)) (:vl-typedef (vl-typedef->comments x)) (otherwise (impossible))))))
Theorem:
(defthm vl-commentmap-p-of-vl-description->comments (b* ((comments (vl-description->comments x))) (vl-commentmap-p comments)) :rule-classes :rewrite)