Make a fast-alist for use with fast-memberp.
(make-lookup-alist x) → ans
(make-lookup-alist x) produces a fast-alist binding every
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.
(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)))
(defthm alistp-of-make-lookup-alist (b* ((ans (make-lookup-alist x))) (alistp ans)) :rule-classes :rewrite)
(defthm hons-assoc-equal-of-make-lookup-alist (iff (hons-assoc-equal a (make-lookup-alist x)) (member-equal a (double-rewrite x))))
(defthm consp-of-make-lookup-alist (equal (consp (make-lookup-alist x)) (consp x)))
(defthm make-lookup-alist-under-iff (iff (make-lookup-alist x) (consp x)))
(defthm strip-cars-of-make-lookup-alist (equal (strip-cars (make-lookup-alist x)) (list-fix x)))
(defthm alist-keys-of-make-lookup-alist (equal (alist-keys (make-lookup-alist x)) (list-fix x)))