Standard-co
The character output channel to which ld prints
Standard-co is an ld special (see ld). The
accessor is (standard-co state) and the updater is (set-standard-co
val state). Standard-co must be an open character output channel. It
is to this channel that ld prints the prompt, the form to be
evaluated, and the results. The event commands such as defun,
defthm, etc., which print extensive commentary do not print to
standard-co but rather to a different channel, proofs-co, so that
you may redirect this commentary while still interacting via standard-co.
See proofs-co.
``Standard-co'' stands for ``standard character output.'' The initial value
of standard-co is the same as the value of *standard-co*.
