membership predicate, using 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.