Print-object$+
Print an object to an open output channel in a specified manner
General Form:
(print-object$+ x ; an ACL2 object
channel ; an open object output channel
&key
header ; nil or a comment string (see below)
serialize-character ; as in @(see with-serialize-character)
print-base print-case ... ; print-control variables
)
This macro is a more flexible variant of print-object$. Any of the
print-control variables may be provided as a keyword; see print-control. All arguments are evaluated.
The :header is printed so that it immediately precedes x. By
default, a single newline is what is printed for the header. If :header
is specified as nil then no such header is printed. Otherwise, the value
:header should be a string for which the first non-whitespace character
(if any) on each line is a semicolon (;). If the last character of the
string is not a newline, then a newline will be printed to separate the string
from x.
The :serialize-character keyword argument has a default of nil.
If it is supplied a value other than nil or 'nil (even if it is
supplied an expression other than those two constants), then it is an error to
supply other keyword arguments. Otherwise printing is done without
serialization (see serialize).
