Print-specifier
Specifies the screen output printed by an APT transformation.
A print specifier is passed as the :print input to a transformation.
It must be one of the following:
- nil, to print nothing (not even error output).
- :error, to print only error output (if any).
- :result, to print,
besides error output,
the generated functions and theorems
described in reference documentation of the transformation,
i.e. the result of the transformation.
This is the default value of the :print input.
- :info, to print,
besides error output and the result (see :result above),
some additional information
about the operations performed by the transformation.
- :all, to print,
besides error output,
the result,
and the additional information (see :info above),
also ACL2's output in response to all the submitted events
(the ones that form the result as well as some ancillary ones).
If the call to the transformation is
redundant,
a message to that effect is printed on the screen,
unless :print is nil.
