Recognizes the associative/commutative binary vl-op-ps.
This is an ordinary defenum.
Function:
(defun vl-op-ac-p (x) (declare (xargs :guard t)) (or (eq x ':vl-binary-plus) (eq x ':vl-binary-logand) (eq x ':vl-binary-logor) (eq x ':vl-binary-bitand) (eq x ':vl-binary-bitor) (eq x ':vl-binary-xor) (eq x ':vl-binary-xnor)))
Theorem: type-when-vl-op-ac-p
(defthm type-when-vl-op-ac-p (implies (vl-op-ac-p x) (if (symbolp x) (if (not (equal x 't)) (not (equal x 'nil)) 'nil) 'nil)) :rule-classes :compound-recognizer)