		Search-engine friendly clone of the ACL2 documentation.

Event-macro-input-processors

Evmac-process-input-print

Process the :print input of an event macro.

Signature
(evmac-process-input-print print ctx state) → (mv erp print$ state)
Returns: print$ — Type (evmac-input-print-p print$).

This is for event macros that have a :print input to specify what is printed on the screen when the even macro is run.

If the :print input, is valid, it is returned unchanged. This facilitates guard/type proofs involving this function, by obviating the need to enable this function in such proofs to establish that, if the :print input passes validation, then it satisfies evmac-input-print-p.

Definitions and Theorems

Function: evmac-process-input-print

(defun evmac-process-input-print (print ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'evmac-process-input-print))
  (declare (ignorable __function__))
  (if (evmac-input-print-p print)
      (value print)
   (er-soft+
    ctx t nil
    "The :PRINT input must be ~
               NIL, :ERROR, :RESULT, :INFO, or :ALL; ~
               but it is ~x0 instead."
    print))))

Theorem: evmac-input-print-p-of-evmac-process-input-print.print$

(defthm evmac-input-print-p-of-evmac-process-input-print.print$
  (b* (((mv ?erp ?print$ ?state)
        (evmac-process-input-print print ctx state)))
    (evmac-input-print-p print$))
  :rule-classes :rewrite)