(vl-module-elimalways x) → new-x
Function:
(defun vl-module-elimalways (x) (declare (xargs :guard (vl-module-p x))) (let ((__function__ 'vl-module-elimalways)) (declare (ignorable __function__)) (b* ((x (vl-module-fix x)) ((vl-module x) x) ((when (vl-module->hands-offp x)) x) ((unless x.alwayses) x) (warnings (vl-warn-about-bad-always-blocks x.alwayses x.warnings))) (change-vl-module x :alwayses nil :warnings warnings))))
Theorem:
(defthm vl-module-p-of-vl-module-elimalways (b* ((new-x (vl-module-elimalways x))) (vl-module-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-module-elimalways-of-vl-module-fix-x (equal (vl-module-elimalways (vl-module-fix x)) (vl-module-elimalways x)))
Theorem:
(defthm vl-module-elimalways-vl-module-equiv-congruence-on-x (implies (vl-module-equiv x x-equiv) (equal (vl-module-elimalways x) (vl-module-elimalways x-equiv))) :rule-classes :congruence)