		Search-engine friendly clone of the ACL2 documentation.

Clean-params

Vl-modulelist-clean-params-loop

Signature
(vl-modulelist-clean-params-loop x n) → new-x
Arguments: x — Guard (vl-modulelist-p x).; n — Guard (natp n).
Returns: new-x — Type (vl-modulelist-p new-x), given the guard.

Definitions and Theorems

Function: vl-modulelist-clean-params-loop

(defun vl-modulelist-clean-params-loop (x n)
 (declare (xargs :guard (and (vl-modulelist-p x) (natp n))))
 (let ((__function__ 'vl-modulelist-clean-params-loop))
  (declare (ignorable __function__))
  (b*
   (((when (zp n))
     (cw
      "Warning: ran out of passes in vl-modulelist-clean-params-loop.~%")
     x)
    ((mv x-prime map)
     (vl-modulelist-clean-params-aux x))
    ((unless map) x)
    (x-prime (vl-modulelist-elim-useless-params x-prime map))
    (- (fast-alist-free map)))
   (vl-modulelist-clean-params-loop x-prime (- n 1)))))

Theorem: vl-modulelist-p-of-vl-modulelist-clean-params-loop

(defthm vl-modulelist-p-of-vl-modulelist-clean-params-loop
  (implies (and (force (vl-modulelist-p x))
                (force (natp n)))
           (b* ((new-x (vl-modulelist-clean-params-loop x n)))
             (vl-modulelist-p new-x)))
  :rule-classes :rewrite)