		Search-engine friendly clone of the ACL2 documentation.

Assoc-string-equal

Look up key, a string, in association list

(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.

Function: assoc-string-equal

(defun assoc-string-equal (str alist)
  (declare (xargs :guard (and (stringp str)
                              (string-alistp alist))))
  (cond ((endp alist) nil)
        ((string-equal str (car (car alist)))
         (car alist))
        (t (assoc-string-equal str (cdr alist)))))