Examples: (set-inhibit-output-lst '(warning)) (set-inhibit-output-lst '(proof-tree prove proof-builder)) (set-inhibit-output-lst *valid-output-names*) ; inhibit all prover output :set-inhibit-output-lst (proof-tree prove) General Form: (set-inhibit-output-lst x)
error error messages (but for hard errors, see below) 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-builder commentary produced by the interactive proof-builder event non-proof commentary produced by events such as defun and encapsulate history output from history commands such as :ubt and :pbt summary the summary at the successful conclusion of an event proof-tree proof-tree output comment output from cw, cw!, and utilities like time$ that use them
It is possible to inhibit each kind of output by putting the corresponding
Note that proof output can be controlled without inhibiting it using this utility, and indeed is already quite limited by default. See set-gag-mode.
See with-output for a variant of this utility that can be used in books. Also see set-inhibit-warnings and set-inhibit-er for how to inhibit individual warning and error output types, respectively, and see set-inhibited-summary-types for how to inhibit individual parts of the summary.
Printing of events on behalf of certify-book and encapsulate is inhibited when both
Normally, hard error messages (see er) are not inhibited. To
inhibit those as well when
To get the current of names representing kinds of inhibit output, evaluate
Note for advanced users. By including