Enumeration of booleans and
This is an ordinary std::defenum.
Function:
(defun t/nil/auto-p (x) (declare (xargs :guard t)) (or (eq x 't) (eq x 'nil) (eq x ':auto)))
Theorem: type-when-t/nil/auto-p
(defthm type-when-t/nil/auto-p (implies (t/nil/auto-p x) (symbolp x)) :rule-classes :compound-recognizer)