Member
Membership predicate
General Forms:
(member x lst)
(member x lst :test 'eql) ; same as above (eql as equality test)
(member x lst :test 'eq) ; same, but eq is equality test
(member x lst :test 'equal) ; same, but equal is equality test
(Member x lst) equals the longest tail of the list lst that
begins with x, or else nil if no such tail exists. The optional
keyword, :TEST, has no effect logically, but provides the test (default
eql) used for comparing x with successive elements of
lst.
The guard for a call of member depends on the test. In all
cases, the second argument must satisfy true-listp. If the test is
eql, then either the first argument must be suitable for eql
(see eqlablep) or the second argument must satisfy eqlable-listp. If the test is eq, then either the first argument
must be a symbol or the second argument must satisfy symbol-listp.
See equality-variants for a discussion of the relation between
member and its variants:
(member-eq x lst) is equivalent to (member x lst :test
'eq);
(member-equal x lst) is equivalent to (member x lst :test
'equal).
In particular, reasoning about any of these primitives reduces to reasoning
about the function member-equal.
Member is defined by Common Lisp. See any Common Lisp documentation
for more information.
Function: member-equal
(defun member-equal (x lst)
(declare (xargs :guard (true-listp lst)))
(cond ((endp lst) nil)
((equal x (car lst)) lst)
(t (member-equal x (cdr lst)))))Subtopics
- Std/lists/member
- Lemmas about member available in the std/lists
library.
