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

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

(Assoc-eq x alist) is provably the same in the ACL2 logic as (assoc x alist) and (assoc-equal x alist), but it has a stronger guard because it uses eq for a more efficient test for whether x is equal to a given key of alist. Its guard requires that alist is an association list (see alistp), and moreover, either x is a symbol or all keys of alist are symbols, i.e., alist is a symbol-alistp.