eql as test
Major Section: PROGRAMMING
(Member x l) equals the longest tail of l that begins with
x, or else nil if no such tail exists.
(Member x l) is provably the same in the ACL2 logic as
(member-equal x l). It has a stronger guard than member-equal
because uses eql to test for whether x is equal to a given
member of l. Its guard requires that l is a true list, and
moreover, either (eqlablep x) or all members of l are
eqlablep. See member-equal and see member-eq.
Member is a Common Lisp function. See any Common Lisp
documentation for more information. Since ACL2 functions cannot
take keyword arguments (though macros can), the ACL2 functions
member-equal and member-eq are defined to correspond to calls
of the Common Lisp function member whose keyword argument
:test is equal or eq, respectively.
