run instructions with output
Major Section: PROOF-CHECKER-COMMANDS
Example: (noise induct prove)Run the
General Form: (noise &rest instruction-list)
instruction-listthrough the top-level loop with output.
In fact, having output is the default.
Noise is useful inside a
surrounding call of
quiet, when one temporarily wants output. For
example, if one wants to see output for a
prove command immediately
induct command but before an
s command, one may want to
submit an instruction like
(quiet induct (noise prove) s). See also