		Search-engine friendly clone of the ACL2 documentation.

Event-macros

Restore-output?

Conditionally wrap an event form to have it produce screen output according to previously saved screen output settings.

Signature
(restore-output? yes/no event) → new-event
Arguments: yes/no — Guard (booleanp yes/no).; event — Guard (pseudo-event-formp event).
Returns: new-event — Type (pseudo-event-formp new-event), given (pseudo-event-formp event).

This leaves the form unchanged if the boolean is nil, otherwise it calls restore-output on it.

Definitions and Theorems

Function: restore-output?

(defun restore-output? (yes/no event)
       (declare (xargs :guard (and (booleanp yes/no)
                                   (pseudo-event-formp event))))
       (let ((__function__ 'restore-output?))
            (declare (ignorable __function__))
            (if yes/no (restore-output event)
                event)))

Theorem: pseudo-event-formp-of-restore-output?

(defthm pseudo-event-formp-of-restore-output?
        (implies (pseudo-event-formp event)
                 (b* ((new-event (restore-output? yes/no event)))
                     (pseudo-event-formp new-event)))
        :rule-classes :rewrite)