Determine the indices of useless parameters.
(vl-positions-of-params names paramdecls) → *
Function:
(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:
(defthm integer-listp-of-vl-positions-of-params (integer-listp (vl-positions-of-params names paramdecls)))