		Search-engine friendly clone of the ACL2 documentation.

Evmac-input-print-p

Evmac-input-print-<=

Less-than-or-equal-to ordering on print levels.

Signature
(evmac-input-print-<= x y) → yes/no
Arguments: x — Guard (evmac-input-print-p x).; y — Guard (evmac-input-print-p y).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: evmac-input-print-<=

(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__))
    (or (evmac-input-print-< x y)
        (equal x y))))

Theorem: booleanp-of-evmac-input-print-<=

(defthm booleanp-of-evmac-input-print-<=
  (b* ((yes/no (evmac-input-print-<= x y)))
    (booleanp yes/no))
  :rule-classes :rewrite)