STANDARD-CO

the character output channel to which 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*).