		Search-engine friendly clone of the ACL2 documentation.

Hons-member-equal

MEMBER-EQUAL using HONS-EQUAL for each equality check

Definitions and Theorems

Function: hons-member-equal

(defun hons-member-equal (x y)
  (declare (xargs :guard t))
  (mbe :logic (member-equal x y)
       :exec (cond ((atom y) nil)
                   ((hons-equal x (car y)) y)
                   (t (hons-member-equal x (cdr y))))))