		Search-engine friendly clone of the ACL2 documentation.

User-interface

Suppress-output

Wrap an event form with a construct to suppress its output.

Signature
(suppress-output form) → form-with-output-suppressed
Arguments: form — Guard (pseudo-event-formp form).
Returns: form-with-output-suppressed — Type (pseudo-event-formp form-with-output-suppressed).

Definitions and Theorems

Function: suppress-output

(defun suppress-output (form)
 (declare (xargs :guard (pseudo-event-formp form)))
 (let ((__function__ 'suppress-output))
  (declare (ignorable __function__))
  (cons
   'with-output
   (cons
      ':gag-mode
      (cons 'nil
            (cons ':off
                  (cons ':all
                        (cons ':on
                              (cons 'error (cons form 'nil))))))))))

Theorem: pseudo-event-formp-of-suppress-output

(defthm pseudo-event-formp-of-suppress-output
  (b* ((form-with-output-suppressed (suppress-output form)))
    (pseudo-event-formp form-with-output-suppressed))
  :rule-classes :rewrite)