ACL2-pc::noise
(meta)
run instructions with prover output
Example:
(noise induct prove)
General Form:
(noise &rest instruction-list)
Run the instruction-list through the top-level loop with prover
output.
In fact, having prover 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). Also see
ACL2-pc::quiet and ACL2-pc::noise!.
