ASSOC

look up key in association list, using eql as test
Major Section:  PROGRAMMING

(Assoc x alist) is the first member of alist whose car is x, or nil if no such member exists.

(Assoc x alist) is provably the same in the ACL2 logic as (assoc-equal x alist). It has a stronger guard than assoc-equal because it uses eql to test whether x is equal to the car of a given member of alist. Its guard requires that alist is an alistp, and moreover, either (eqlablep x) or all cars of members of alist are eqlablep. See assoc-equal and see assoc-eq.

Assoc 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 assoc-equal and assoc-eq are defined to correspond to calls of the Common Lisp function assoc whose keyword argument :test is equal or eq, respectively.