(vl-design-combinational-elim x) → new-x
Function:
(defun vl-design-combinational-elim (x) (declare (xargs :guard (vl-design-p x))) (let ((__function__ 'vl-design-combinational-elim)) (declare (ignorable __function__)) (b* (((vl-design x) x) (new-mods (vl-modulelist-combinational-elim x.mods))) (change-vl-design x :mods new-mods))))
Theorem:
(defthm vl-design-p-of-vl-design-combinational-elim (b* ((new-x (vl-design-combinational-elim x))) (vl-design-p new-x)) :rule-classes :rewrite)