look up key in a keyword-value-listp
Major Section:  ACL2-BUILT-INS

If l is a list of even length of the form (k1 a1 k2 a2 ... kn an), where each ki is a keyword, then (assoc-keyword key l) is the first tail of l starting with key if key is some ki, and is nil otherwise.

The guard for (assoc-keyword key l) is (keyword-value-listp l).

To see the ACL2 definition of this function, see pf.