Print an an object to an open output channel
(print-object$ x channel state)
where x is any ACL2 object and channel is an open output
channel. See io.
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
For a related utility, see write-list.