		Search-engine friendly clone of the ACL2 documentation.

Clean-params

Vl-module-elim-useless-params

Signature
(vl-module-elim-useless-params x map) → new-x
Arguments: x — Guard (vl-module-p x).; map — Guard (vl-useless-params-map-p map).
Returns: new-x — Type (vl-module-p new-x), given the guard.

Definitions and Theorems

Function: vl-module-elim-useless-params

(defun vl-module-elim-useless-params (x map)
 (declare (xargs :guard (and (vl-module-p x)
                             (vl-useless-params-map-p map))))
 (let ((__function__ 'vl-module-elim-useless-params))
   (declare (ignorable __function__))
   (let*
      ((modinsts (vl-module->modinsts x))
       (modinsts (vl-modinstlist-elim-useless-params modinsts map)))
     (change-vl-module x
                       :modinsts modinsts))))

Theorem: vl-module-p-of-vl-module-elim-useless-params

(defthm vl-module-p-of-vl-module-elim-useless-params
  (implies (and (force (vl-module-p x))
                (force (vl-useless-params-map-p map)))
           (b* ((new-x (vl-module-elim-useless-params x map)))
             (vl-module-p new-x)))
  :rule-classes :rewrite)

Theorem: vl-module->name-of-vl-module-elim-useless-params

(defthm vl-module->name-of-vl-module-elim-useless-params
  (equal (vl-module->name (vl-module-elim-useless-params x map))
         (vl-module->name x)))