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.
