		Search-engine friendly clone of the ACL2 documentation.

Standard-string-alistp

Recognizer for association lists with standard strings as keys

(Standard-string-alistp x) is true if and only if x is a list of pairs of the form (cons key val) where key is a string all of whose characters are standard (see standard-char-p).

Standard-string-alistp has a guard of t.

Function: standard-string-alistp

(defun standard-string-alistp (x)
       (declare (xargs :guard t))
       (cond ((atom x) (eq x nil))
             (t (and (consp (car x))
                     (stringp (car (car x)))
                     (standard-string-p (car (car x)))
                     (standard-string-alistp (cdr x))))))