ld prints
Major Section: ACL2-BUILT-INS
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* (see *standard-co*).
