		Search-engine friendly clone of the ACL2 documentation.

Clean-params

Vl-position-of-param

Determine the index of a useless parameter.

Signature
(vl-position-of-param name paramdecls) → *
Arguments: name — Guard (stringp name).; paramdecls — Guard (vl-paramdecllist-p paramdecls).

We use this to construct the vl-useless-params-p structure after identifying the names of the useless parameters.

Definitions and Theorems

Function: vl-position-of-param

(defun vl-position-of-param (name paramdecls)
 (declare (xargs :guard (and (stringp name)
                             (vl-paramdecllist-p paramdecls))))
 (declare
   (xargs
        :guard (member-equal name
                             (vl-paramdecllist->names paramdecls))))
 (let ((__function__ 'vl-position-of-param))
   (declare (ignorable __function__))
   (cond ((atom paramdecls)
          (progn$ (impossible) 0))
         ((equal name
                 (vl-paramdecl->name (car paramdecls)))
          0)
         (t (+ 1
               (vl-position-of-param name (cdr paramdecls)))))))