		Search-engine friendly clone of the ACL2 documentation.

Utilities

Make-lookup-alist

Make a fast-alist for use with fast-memberp.

Signature
(make-lookup-alist x) → ans
Returns: ans — Type (alistp ans).

(make-lookup-alist x) produces a fast-alist binding every member of x to t.

Constructing a lookup alist allows you to use fast-memberp in lieu of member or member-equal, which may be quite a lot faster on large lists.

Don't forget to free the alist after you are done using it, via fast-alist-free.

Definitions and Theorems

Function: make-lookup-alist

(defun make-lookup-alist (x)
  (declare (xargs :guard t))
  (let ((__function__ 'make-lookup-alist))
    (declare (ignorable __function__))
    (if (consp x)
        (hons-acons (car x)
                    t (make-lookup-alist (cdr x)))
      nil)))

Theorem: alistp-of-make-lookup-alist

(defthm alistp-of-make-lookup-alist
  (b* ((ans (make-lookup-alist x)))
    (alistp ans))
  :rule-classes :rewrite)

Theorem: hons-assoc-equal-of-make-lookup-alist

(defthm hons-assoc-equal-of-make-lookup-alist
  (iff (hons-assoc-equal a (make-lookup-alist x))
       (member-equal a (double-rewrite x))))

Theorem: consp-of-make-lookup-alist

(defthm consp-of-make-lookup-alist
  (equal (consp (make-lookup-alist x))
         (consp x)))

Theorem: make-lookup-alist-under-iff

(defthm make-lookup-alist-under-iff
  (iff (make-lookup-alist x) (consp x)))

Theorem: strip-cars-of-make-lookup-alist

(defthm strip-cars-of-make-lookup-alist
  (equal (strip-cars (make-lookup-alist x))
         (list-fix x)))

Theorem: alist-keys-of-make-lookup-alist

(defthm alist-keys-of-make-lookup-alist
  (equal (alist-keys (make-lookup-alist x))
         (list-fix x)))