## SET-INHIBIT-OUTPUT-LST

control output
Major Section: OTHER

Examples:
(set-inhibit-output-lst '(warning))
(set-inhibit-output-lst '(proof-tree prove proof-checker))
:set-inhibit-output-lst (proof-tree prove)
General Form:
(set-inhibit-output-lst lst)

where `lst`

is a form (which may mention `state`

) that evaluates
to a list of names, each of which is the name of one of the
following ``kinds'' of output produced by ACL2.
error error messages
warning warnings other than those related to soundness
warning! warnings (of all degrees of importance)
observation observations
prove commentary produced by the theorem prover
proof-checker commentary produced by the proof-checker
event non-proof commentary produced by events such as defun
and encapsulate
expansion commentary produced by make-event expansion
summary the summary at the successful conclusion of an event
proof-tree proof-tree output

It is possible to inhibit each kind of output by putting the
corresponding name into `lst`

. For example, if `'warning`

is
included in (the value of) `lst`

, then no warnings are printed
except those related to soundness, e.g., the inclusion of an
uncertified book. Note that proof-tree output is affected by
`set-inhibit-output-lst`

; see proof-tree.
Printing of events on behalf of `certify-book`

, `encapsulate`

,
or `defstobj`

is inhibited when both `'event`

and `'prove`

belong to `lst`

. Otherwise, printing of events is controlled by
the `ld`

special `ld-pre-eval-print`

.