		Search-engine friendly clone of the ACL2 documentation.

Member-eql-without-truelistp

Signature
(member-eql-without-truelistp a x) → *
Arguments: a — Guard (eqlablep a).

Definitions and Theorems

Function: member-eql-without-truelistp

(defun member-eql-without-truelistp (a x)
 (declare (xargs :guard (eqlablep a)))
 (let ((__function__ 'member-eql-without-truelistp))
   (declare (ignorable __function__))
   (mbe :logic (member a x)
        :exec (cond ((atom x) nil)
                    ((eql a (car x)) x)
                    (t (member-eql-without-truelistp a (cdr x)))))))