MEMBER-EQ

Major Section:  PROGRAMMING

(Member-eq x lst) equals the longest tail of lst that begins with x, or else nil if no such tail exists.

(Member-eq x lst) is provably the same in the ACL2 logic as (member x lst) and (member-equal x lst), but it has a stronger guard because it uses eq for a more efficient test for whether x is equal to a given member of lst. Its guard requires that lst is a true list, and moreover, either x is a symbol or lst is a list of symbols. See member-equal and see member.