the proofs character output channel
Major Section:  ACL2-BUILT-INS

Proofs-co is an ld special (see ld). The accessor is (proofs-co state) and the updater is (set-proofs-co val state). Proofs-co must be an open character output channel. It is to this channel that defun, defthm, and the other event commands print their commentary.

``Proofs-co'' stands for ``proofs character output.'' The initial value of proofs-co is the same as the value of *standard-co* (see *standard-co*).