		Search-engine friendly clone of the ACL2 documentation.

Expressions

Vl-op-p

Recognizer for valid operators.

Signature
(vl-op-p x) → *

(vl-op-p x) checks that x is one of the operators listed in the *vl-ops-table*. We prefer to use vl-op-p instead of looking up operators directly in the table, since this way we can disable vl-op-p and avoid large case splits.

Definitions and Theorems

Function: vl-op-p$inline

(defun vl-op-p$inline (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-op-p))
    (declare (ignorable __function__))
    (if (assoc x (vl-ops-table)) t nil)))

Theorem: type-when-vl-op-p

(defthm type-when-vl-op-p
  (implies (vl-op-p x)
           (and (symbolp x)
                (not (equal x t))
                (not (equal x nil))))
  :rule-classes :compound-recognizer)

Theorem: vl-opinfo-p-of-lookup-when-vl-op-p

(defthm vl-opinfo-p-of-lookup-when-vl-op-p
 (implies
     (vl-op-p x)
     (and (vl-opinfo-p (cdr (assoc x (vl-ops-table))))
          (vl-opinfo-p (cdr (hons-assoc-equal x (vl-ops-table)))))))

Subtopics

Vl-op-fix