		Search-engine friendly clone of the ACL2 documentation.

Vl-casestmt

Vl-casecheck-p

Case statement violation checking mode.

For ordinary case statements this will be nil. The other values are for SystemVerilog's unique, unique0, and priority case statements.

This is an ordinary defenum.

Function: vl-casecheck-p

(defun vl-casecheck-p (x)
  (declare (xargs :guard t))
  (or (eq x 'nil)
      (eq x ':vl-unique)
      (eq x ':vl-unique0)
      (eq x ':vl-priority)))

Theorem: type-when-vl-casecheck-p

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