		Search-engine friendly clone of the ACL2 documentation.

Lex-keywords

Vl-full-keyword-table

A fast alist binding all currently supported keyword names to their corresponding :vl-kwd-xxx symbols.

Signature
(vl-full-keyword-table) → *

Definitions and Theorems

Function: vl-full-keyword-table

(defun vl-full-keyword-table nil
  (declare (xargs :guard t))
  (let ((__function__ 'vl-full-keyword-table))
    (declare (ignorable __function__))
    *vl-2012-keyword-table*))

Theorem: symbol-listp-of-alist-vals-of-vl-full-keyword-table

(defthm symbol-listp-of-alist-vals-of-vl-full-keyword-table
  (symbol-listp (alist-vals (vl-full-keyword-table))))

Theorem: symbolp-of-lookup-in-vl-full-keyword-table

(defthm symbolp-of-lookup-in-vl-full-keyword-table
  (symbolp (cdr (hons-assoc-equal key (vl-full-keyword-table)))))