		Search-engine friendly clone of the ACL2 documentation.

Vl-simplify-main

Vl-simplify-maybe-clean-params

Wrapper to hide the case split for optional clean-params.

Signature
(vl-simplify-maybe-clean-params design config) → new-design
Arguments: design — Guard (vl-design-p design).; config — Guard (vl-simpconfig-p config).
Returns: new-design — Type (vl-design-p new-design).

Definitions and Theorems

Function: vl-simplify-maybe-clean-params

(defun vl-simplify-maybe-clean-params (design config)
  (declare (xargs :guard (and (vl-design-p design)
                              (vl-simpconfig-p config))))
  (let ((__function__ 'vl-simplify-maybe-clean-params))
    (declare (ignorable __function__))
    (b* (((vl-simpconfig config) config)
         ((unless config.clean-params-p)
          (vl-design-fix design)))
      (xf-cwtime (vl-design-clean-params design)))))

Theorem: vl-design-p-of-vl-simplify-maybe-clean-params

(defthm vl-design-p-of-vl-simplify-maybe-clean-params
  (b* ((new-design (vl-simplify-maybe-clean-params design config)))
    (vl-design-p new-design))
  :rule-classes :rewrite)