		Search-engine friendly clone of the ACL2 documentation.

Utilities

Vl-string-keys-p

Recognizer for alists whose keys are strings.

Definitions and Theorems

Function: vl-string-keys-p

(defun vl-string-keys-p (x)
  (declare (xargs :guard t))
  (if (consp x)
      (and (consp (car x))
           (stringp (caar x))
           (vl-string-keys-p (cdr x)))
    (not x)))

Theorem: vl-string-keys-p-when-not-consp

(defthm vl-string-keys-p-when-not-consp
  (implies (not (consp x))
           (equal (vl-string-keys-p x) (not x))))

Theorem: vl-string-keys-p-of-cons

(defthm vl-string-keys-p-of-cons
  (equal (vl-string-keys-p (cons a x))
         (and (consp a)
              (stringp (car a))
              (vl-string-keys-p x))))

Theorem: vl-string-keys-p-of-hons-shrink-alist

(defthm vl-string-keys-p-of-hons-shrink-alist
  (implies (and (vl-string-keys-p x)
                (vl-string-keys-p ans))
           (vl-string-keys-p (hons-shrink-alist x ans))))

Theorem: string-listp-of-strip-cars-when-vl-string-keys-p

(defthm string-listp-of-strip-cars-when-vl-string-keys-p
  (implies (vl-string-keys-p x)
           (string-listp (strip-cars x))))

Theorem: vl-string-keys-p-of-make-lookup-alist

(defthm vl-string-keys-p-of-make-lookup-alist
  (equal (vl-string-keys-p (make-lookup-alist x))
         (string-listp (list-fix x))))