Conditionally wrap an event form to have it produce screen output according to previously saved screen output settings.
This leaves the form unchanged if the boolean is
(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)))
(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)