		Search-engine friendly clone of the ACL2 documentation.

Vl-description

Vl-fast-find-description

Signature
(vl-fast-find-description name descriptions descalist) → *
Arguments: name — Guard (stringp name).; descriptions — Guard (vl-descriptionlist-p descriptions).; descalist — Guard (equal descalist (vl-make-descalist descriptions)).

Definitions and Theorems

Function: vl-fast-find-description$inline

(defun vl-fast-find-description$inline (name descriptions descalist)
 (declare
      (xargs :guard (and (stringp name)
                         (vl-descriptionlist-p descriptions)
                         (equal descalist
                                (vl-make-descalist descriptions)))))
 (let ((__function__ 'vl-fast-find-description))
   (declare (ignorable __function__))
   (mbe :logic (vl-find-description name descriptions)
        :exec (cdr (hons-get name descalist)))))