		Search-engine friendly clone of the ACL2 documentation.

Utilities

Vl-string-list-values-p

Recognizer for alists whose values are string lists.

Definitions and Theorems

Function: vl-string-list-values-p

(defun vl-string-list-values-p (x)
  (declare (xargs :guard t))
  (if (consp x)
      (and (consp (car x))
           (string-listp (cdar x))
           (vl-string-list-values-p (cdr x)))
    (not x)))

Theorem: vl-string-list-values-p-when-not-consp

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

Theorem: vl-string-list-values-p-of-cons

(defthm vl-string-list-values-p-of-cons
  (equal (vl-string-list-values-p (cons a x))
         (and (consp a)
              (string-listp (cdr a))
              (vl-string-list-values-p x))))

Theorem: vl-string-list-values-p-of-hons-shrink-alist

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

Theorem: string-listp-of-cdr-of-hons-assoc-equal-when-vl-string-list-values-p

(defthm
 string-listp-of-cdr-of-hons-assoc-equal-when-vl-string-list-values-p
 (implies (vl-string-list-values-p x)
          (string-listp (cdr (hons-assoc-equal a x)))))