		Search-engine friendly clone of the ACL2 documentation.

Argresolve

Vl-fast-find-namedarg

Faster version of vl-find-namedarg, where the search is done as an fast-alist lookup rather than as string search.

Signature
(vl-fast-find-namedarg name namedargs alist) → *
Arguments: name — Guard (stringp name).; namedargs — Guard (vl-namedarglist-p namedargs).; alist — Guard (equal alist (vl-make-namedarg-alist namedargs)).

Definitions and Theorems

Function: vl-fast-find-namedarg

(defun vl-fast-find-namedarg (name namedargs alist)
 (declare
    (xargs :guard (and (stringp name)
                       (vl-namedarglist-p namedargs)
                       (equal alist
                              (vl-make-namedarg-alist namedargs)))))
 (let ((__function__ 'vl-fast-find-namedarg))
   (declare (ignorable __function__))
   (mbe :logic (vl-find-namedarg name namedargs)
        :exec (cdr (hons-get name alist)))))