Recognizes the possible kinds of case statements.
This is an ordinary defenum.
Function:
(defun vl-casetype-p (x) (declare (xargs :guard t)) (or (eq x 'nil) (eq x ':vl-casex) (eq x ':vl-casez)))
Theorem: type-when-vl-casetype-p
(defthm type-when-vl-casetype-p (implies (vl-casetype-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)