		Search-engine friendly clone of the ACL2 documentation.

Lexstate

Vl-plaintoken-alistp

Recognize alists binding strings to plaintoken types.

Signature
(vl-plaintoken-alistp x) → *

We use these for configurable operator handling, based on the particular standard we're implementing.

Definitions and Theorems

Function: vl-plaintoken-alistp

(defun vl-plaintoken-alistp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-plaintoken-alistp))
    (declare (ignorable __function__))
    (if (atom x)
        t
      (and (consp (car x))
           (stringp (caar x))
           (not (equal (caar x) ""))
           (vl-plaintokentype-p (cdar x))
           (vl-plaintoken-alistp (cdr x))))))

Theorem: vl-plaintoken-alistp-when-atom

(defthm vl-plaintoken-alistp-when-atom
  (implies (atom x)
           (equal (vl-plaintoken-alistp x) t)))

Theorem: vl-plaintoken-alistp-of-cons

(defthm vl-plaintoken-alistp-of-cons
  (equal (vl-plaintoken-alistp (cons a x))
         (and (consp a)
              (stringp (car a))
              (not (equal (car a) ""))
              (vl-plaintokentype-p (cdr a))
              (vl-plaintoken-alistp x))))

Theorem: vl-plaintoken-alistp-of-append

(defthm vl-plaintoken-alistp-of-append
  (equal (vl-plaintoken-alistp (append x y))
         (and (vl-plaintoken-alistp x)
              (vl-plaintoken-alistp y))))

Theorem: vl-plaintokentype-p-of-hons-assoc-equal-when-vl-plaintoken-alistp

(defthm
  vl-plaintokentype-p-of-hons-assoc-equal-when-vl-plaintoken-alistp
  (implies
       (vl-plaintoken-alistp x)
       (equal (vl-plaintokentype-p (cdr (hons-assoc-equal key x)))
              (if (hons-assoc-equal key x) t nil))))