		Search-engine friendly clone of the ACL2 documentation.

User-interface

Maybe-suppress-output

Conditionally wrap an event form with a construct to suppress its output.

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

If suppress is non-nil, wrap the event-form form with a construct to suppress its output. Otherwise, just return form.

Definitions and Theorems

Function: maybe-suppress-output

(defun maybe-suppress-output (suppress form)
  (declare (xargs :guard (pseudo-event-formp form)))
  (let ((__function__ 'maybe-suppress-output))
    (declare (ignorable __function__))
    (if suppress (suppress-output form)
      form)))

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

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