ACL2-PC::NOISE

(meta) run instructions with output
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(noise induct prove)

General Form: (noise &rest instruction-list)

Run the instruction-list through 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 following an induct command but before an s command, one may want to submit an instruction like (quiet induct (noise prove) s). See also quiet.