		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)))