		Search-engine friendly clone of the ACL2 documentation.

Finding-by-name

Vl-fast-find-portdecl

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

Signature
(vl-fast-find-portdecl name portdecls alist) → *
Arguments: name — Guard (stringp name).; portdecls — Guard (vl-portdecllist-p portdecls).; alist — Guard (equal alist (vl-make-portdecl-alist portdecls)).

Definitions and Theorems

Function: vl-fast-find-portdecl

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