		Search-engine friendly clone of the ACL2 documentation.

Utilities

Fast-memberp

Fast list membership using make-lookup-alist.

Signature
(fast-memberp a x alist) → *
Arguments: alist — Guard (equal alist (make-lookup-alist x)).

In the logic, (fast-memberp a x alist) is just a list membership check; we leave fast-memberp enabled and always reason about member-equal instead.

However, our guard requires that alist is the result of running make-lookup-alist on x. Because of this, in the execution, the call of member-equal call is instead carried out using hons-get on the alist, and hence is a hash table lookup.

Definitions and Theorems

Function: fast-memberp$inline

(defun fast-memberp$inline (a x alist)
  (declare (xargs :guard (equal alist (make-lookup-alist x))))
  (let ((__function__ 'fast-memberp))
    (declare (ignorable __function__))
    (mbe :logic (if (member-equal a x) t nil)
         :exec (if (hons-get a alist) t nil))))