Look up key in association list
(assoc x alist)
(assoc x alist :test 'eql) ; same as above (eql as equality test)
(assoc x alist :test 'eq) ; same, but eq is equality test
(assoc x alist :test 'equal) ; same, but equal is equality test
(Assoc x alist) is the first member of alist whose car is
x, or nil if no such member exists. The optional keyword,
:TEST, has no effect logically, but provides the test (default eql) used for comparing x with the cars of successive elements
The guard for a call of assoc depends on the test. In all
cases, the second argument must satisfy alistp. If the test is eql, then either the first argument must be suitable for eql (see
eqlablep) or the second argument must satisfy eqlable-alistp.
If the test is eq, then either the first argument must be a symbol or
the second argument must satisfy symbol-alistp.
See equality-variants for a discussion of the relation between
assoc and its variants:
(assoc-eq x alist) is equivalent to (assoc x alist
(assoc-equal x alist) is equivalent to (assoc x alist :test
In particular, reasoning about any of these primitives reduces to reasoning
about the function assoc-equal.
Assoc is defined by Common Lisp. See any Common Lisp documentation
for more information.
(defun assoc-equal (x alist)
(declare (xargs :guard (alistp alist)))
(cond ((endp alist) nil)
((equal x (car (car alist)))
(t (assoc-equal x (cdr alist)))))
- Theorems about assoc-equal
in the std/alists library.