Less-than ordering on print levels.
(evmac-input-print-< x y) → yes/no
Function:
(defun evmac-input-print-< (x y) (declare (xargs :guard (and (evmac-input-print-p x) (evmac-input-print-p y)))) (let ((__function__ 'evmac-input-print-<)) (declare (ignorable __function__)) (case x ((nil) (or (eq y :error) (eq y :result) (eq y :info) (eq y :all))) (:error (or (eq y :result) (eq y :info) (eq y :all))) (:result (or (eq y :info) (eq y :all))) (:info (eq y :all)) (:all nil))))
Theorem:
(defthm booleanp-of-evmac-input-print-< (b* ((yes/no (evmac-input-print-< x y))) (booleanp yes/no)) :rule-classes :rewrite)