other
(in-package "ACL2")
lookup-equalfunction
(defund lookup-equal (key alist) (declare (xargs :guard (alistp alist))) (cdr (assoc-equal key alist)))
(in-package "ACL2")
(defund lookup-equal (key alist) (declare (xargs :guard (alistp alist))) (cdr (assoc-equal key alist)))