This is an ordinary defenum.
Function:
(defun svtv-inputtype-p (x) (declare (xargs :guard t)) (or (eq x ':input) (eq x ':override-val) (eq x ':override-test)))
Theorem: type-when-svtv-inputtype-p
(defthm type-when-svtv-inputtype-p (implies (svtv-inputtype-p x) (if (symbolp x) (if (not (equal x 't)) (not (equal x 'nil)) 'nil) 'nil)) :rule-classes :compound-recognizer)