		Search-engine friendly clone of the ACL2 documentation.

Clean-params

Vl-positions-of-params

Determine the indices of useless parameters.

Signature
(vl-positions-of-params names paramdecls) → *
Arguments: names — Guard (string-listp names).; paramdecls — Guard (vl-paramdecllist-p paramdecls).

Definitions and Theorems

Function: vl-positions-of-params

(defun vl-positions-of-params (names paramdecls)
 (declare (xargs :guard (and (string-listp names)
                             (vl-paramdecllist-p paramdecls))))
 (declare
  (xargs
       :guard (subsetp-equal names
                             (vl-paramdecllist->names paramdecls))))
 (let ((__function__ 'vl-positions-of-params))
   (declare (ignorable __function__))
   (if (atom names)
       nil
     (cons (vl-position-of-param (car names)
                                 paramdecls)
           (vl-positions-of-params (cdr names)
                                   paramdecls)))))

Theorem: integer-listp-of-vl-positions-of-params

(defthm integer-listp-of-vl-positions-of-params
  (integer-listp (vl-positions-of-params names paramdecls)))