lookup-eq-def - ACL2 Book

other

(in-package "ACL2")

lookup-eqfunction

(defund lookup-eq
  (key alist)
  (declare (xargs :guard (if (symbolp key)
        (alistp alist)
        (symbol-alistp alist))))
  (cdr (assoc-eq key alist)))