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.