		Search-engine friendly clone of the ACL2 documentation.

Delayredux

Vl-design-delayredux

Signature
(vl-design-delayredux x &key vecp state-onlyp) → new-x
Arguments: x — Guard (vl-design-p x).
Returns: new-x — Type (vl-design-p new-x).

Definitions and Theorems

Function: vl-design-delayredux-fn

(defun vl-design-delayredux-fn (x vecp state-onlyp)
 (declare (xargs :guard (vl-design-p x)))
 (let ((__function__ 'vl-design-delayredux))
  (declare (ignorable __function__))
  (b* ((x (vl-design-fix x))
       ((vl-design x) x))
   (change-vl-design
       x
       :mods (vl-modulelist-delayredux x.mods
                                       :vecp vecp
                                       :state-onlyp state-onlyp)))))

Theorem: vl-design-p-of-vl-design-delayredux

(defthm vl-design-p-of-vl-design-delayredux
  (b* ((new-x (vl-design-delayredux-fn x vecp state-onlyp)))
    (vl-design-p new-x))
  :rule-classes :rewrite)