Major Section: ACL2-BUILT-INS
(Assoc-string-equal x alist)
is similar to assoc-equal
.
However, for string x
and alist alist
, the comparison of x
with successive keys in alist
is done using string-equal
rather than equal
.
The guard for assoc-string-equal
requires that x
is a string
and alist
is an alist.
To see the ACL2 definition of this function, see pf.