		Search-engine friendly clone of the ACL2 documentation.

Event-macros

Evmac-input-print-p

Recognize a valid :print input of an event macro.

This is an ordinary std::defenum.

Function: evmac-input-print-p

(defun evmac-input-print-p (x)
  (declare (xargs :guard t))
  (or (eq x 'nil)
      (eq x ':error)
      (eq x ':result)
      (eq x ':info)
      (eq x ':all)))

Theorem: type-when-evmac-input-print-p

(defthm type-when-evmac-input-print-p
  (implies (evmac-input-print-p x)
           (if (if (symbolp x)
                   (if (not (equal x 't))
                       (not (equal x 'nil))
                     'nil)
                 'nil)
               't
             (equal x 'nil)))
  :rule-classes :compound-recognizer)

Subtopics

Evmac-input-print-<: Less-than ordering on print levels.
Evmac-input-print->=: Greater-than-or-equal-to ordering on print levels.
Evmac-input-print->: Greater-than ordering on print levels.
Evmac-input-print-<=: Less-than-or-equal-to ordering on print levels.