		Search-engine friendly clone of the ACL2 documentation.

Lex-keywords

Vl-keyword-table-p

Recognize any valid subset of the vl-full-keyword-table.

Signature
(vl-keyword-table-p x) → *

Definitions and Theorems

Function: vl-keyword-table-p

(defun vl-keyword-table-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-keyword-table-p))
    (declare (ignorable __function__))
    (or (atom x)
        (and (consp (car x))
             (equal (car x)
                    (hons-get (caar x)
                              (vl-full-keyword-table)))
             (vl-keyword-table-p (cdr x))))))

Theorem: vl-keyword-table-p-of-vl-full-keyword-table

(defthm vl-keyword-table-p-of-vl-full-keyword-table
  (vl-keyword-table-p (vl-full-keyword-table)))

Theorem: symbol-listp-of-alist-vals-when-vl-keyword-table-p

(defthm symbol-listp-of-alist-vals-when-vl-keyword-table-p
  (implies (vl-keyword-table-p x)
           (symbol-listp (alist-vals x))))

Theorem: symbolp-of-lookup-when-vl-keyword-table-p

(defthm symbolp-of-lookup-when-vl-keyword-table-p
  (implies (vl-keyword-table-p table)
           (symbolp (cdr (hons-assoc-equal key table)))))