Recognize valid values of the
(output-files-process-inputp x) → yes/no
Function:
(defun output-files-process-inputp (x) (declare (xargs :guard t)) (let ((__function__ 'output-files-process-inputp)) (declare (ignorable __function__)) (and (member-eq x '(nil :print)) t)))
Theorem:
(defthm booleanp-of-output-files-process-inputp (b* ((yes/no (output-files-process-inputp x))) (booleanp yes/no)) :rule-classes :rewrite)