		Search-engine friendly clone of the ACL2 documentation.

Vl-unary

Vl-unaryop-p

Recognizer for basic unary operators.

This is an ordinary defenum.

Function: vl-unaryop-p

(defun vl-unaryop-p (x)
  (declare (xargs :guard t))
  (or (eq x ':vl-unary-plus)
      (eq x ':vl-unary-minus)
      (eq x ':vl-unary-lognot)
      (eq x ':vl-unary-bitnot)
      (eq x ':vl-unary-bitand)
      (eq x ':vl-unary-nand)
      (eq x ':vl-unary-bitor)
      (eq x ':vl-unary-nor)
      (eq x ':vl-unary-xor)
      (eq x ':vl-unary-xnor)
      (eq x ':vl-unary-preinc)
      (eq x ':vl-unary-predec)
      (eq x ':vl-unary-postinc)
      (eq x ':vl-unary-postdec)))

Theorem: type-when-vl-unaryop-p

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