		Search-engine friendly clone of the ACL2 documentation.

Modnamespace

Vl-fast-find-moduleitem

Legacy -- Use scopestack instead. Alternative to vl-find-moduleitem using fast alist lookups.

Signature
(vl-fast-find-moduleitem name x itemalist) → *
Arguments: name — Guard (stringp name).; x — Guard (vl-module-p x).; itemalist — Guard (equal itemalist (vl-make-moditem-alist x)).

Definitions and Theorems

Function: vl-fast-find-moduleitem

(defun vl-fast-find-moduleitem (name x itemalist)
 (declare
   (xargs :guard (and (stringp name)
                      (vl-module-p x)
                      (equal itemalist (vl-make-moditem-alist x)))))
 (let ((__function__ 'vl-fast-find-moduleitem))
   (declare (ignorable __function__))
   (mbe :logic (vl-find-moduleitem name x)
        :exec (cdr (hons-get name itemalist)))))