		Search-engine friendly clone of the ACL2 documentation.

Vl-binary

Vl-binaryop-p

Recognizer for basic binary operators.

This is an ordinary defenum.

Function: vl-binaryop-p

(defun vl-binaryop-p (x)
  (declare (xargs :guard t))
  (or (eq x ':vl-binary-plus)
      (eq x ':vl-binary-minus)
      (eq x ':vl-binary-times)
      (eq x ':vl-binary-div)
      (eq x ':vl-binary-rem)
      (eq x ':vl-binary-eq)
      (eq x ':vl-binary-neq)
      (eq x ':vl-binary-ceq)
      (eq x ':vl-binary-cne)
      (eq x ':vl-binary-wildeq)
      (eq x ':vl-binary-wildneq)
      (eq x ':vl-binary-logand)
      (eq x ':vl-binary-logor)
      (eq x ':vl-binary-power)
      (eq x ':vl-binary-lt)
      (eq x ':vl-binary-lte)
      (eq x ':vl-binary-gt)
      (eq x ':vl-binary-gte)
      (eq x ':vl-binary-bitand)
      (eq x ':vl-binary-bitor)
      (eq x ':vl-binary-xor)
      (eq x ':vl-binary-xnor)
      (eq x ':vl-binary-shr)
      (eq x ':vl-binary-shl)
      (eq x ':vl-binary-ashr)
      (eq x ':vl-binary-ashl)
      (eq x ':vl-binary-assign)
      (eq x ':vl-binary-plusassign)
      (eq x ':vl-binary-minusassign)
      (eq x ':vl-binary-timesassign)
      (eq x ':vl-binary-divassign)
      (eq x ':vl-binary-remassign)
      (eq x ':vl-binary-andassign)
      (eq x ':vl-binary-orassign)
      (eq x ':vl-binary-xorassign)
      (eq x ':vl-binary-shlassign)
      (eq x ':vl-binary-shrassign)
      (eq x ':vl-binary-ashlassign)
      (eq x ':vl-binary-ashrassign)
      (eq x ':vl-implies)
      (eq x ':vl-equiv)))

Theorem: type-when-vl-binaryop-p

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