(vl-module-allexprs-nrev x nrev) → nrev
Function:
(defun vl-module-allexprs-nrev$inline (x nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (vl-module-p x))) (let ((__function__ 'vl-module-allexprs-nrev)) (declare (ignorable __function__)) (b* ((x (vl-module-fix x))) (b* (((vl-module x) x) (nrev (vl-portlist-allexprs-nrev x.ports nrev)) (nrev (vl-portdecllist-allexprs-nrev x.portdecls nrev)) (nrev (vl-assignlist-allexprs-nrev x.assigns nrev)) (nrev (vl-vardecllist-allexprs-nrev x.vardecls nrev)) (nrev (vl-paramdecllist-allexprs-nrev x.paramdecls nrev)) (nrev (vl-fundecllist-allexprs-nrev x.fundecls nrev)) (nrev (vl-taskdecllist-allexprs-nrev x.taskdecls nrev)) (nrev (vl-modinstlist-allexprs-nrev x.modinsts nrev)) (nrev (vl-gateinstlist-allexprs-nrev x.gateinsts nrev)) (nrev (vl-alwayslist-allexprs-nrev x.alwayses nrev)) (nrev (vl-initiallist-allexprs-nrev x.initials nrev)) (nrev (vl-aliaslist-allexprs-nrev x.aliases nrev))) nrev))))
Theorem:
(defthm vl-module-allexprs-nrev$inline-of-vl-module-fix-x (equal (vl-module-allexprs-nrev$inline (vl-module-fix x) nrev) (vl-module-allexprs-nrev$inline x nrev)))
Theorem:
(defthm vl-module-allexprs-nrev$inline-vl-module-equiv-congruence-on-x (implies (vl-module-equiv x x-equiv) (equal (vl-module-allexprs-nrev$inline x nrev) (vl-module-allexprs-nrev$inline x-equiv nrev))) :rule-classes :congruence)