where x is any ACL2 object and channel is an open object output
channel. See io.
Remarks
A newline is printed just above x. To eliminate that newline or print
a given comment instead, see print-object$+.
Print-object$ pays attention to the values of print-control
variables. To provide them as keyword arguments rather than assigning them
globally, see print-object$+.
By default, the output of print-object$ is human-readable. To use
serialize printing instead, first set the serialize character using
set-serialize-character.
