print to the comment window
Major Section:  ACL2-BUILT-INS

See cw for an introduction to the comment window and the usual way to print it.

Function fmt-to-comment-window is identical to fmt1 (see fmt), except that the channel is *standard-co* and the ACL2 state is neither an input nor an output. An analogous function, fmt-to-comment-window!, prints with fmt! instead of fmt, in order to avoid insertion of backslash (\) characters for margins; also see cw!. Note that even if you change the value of ld special standard-co (see standard-co), fmt-to-comment-window will print to *standard-co*, which is the original value of standard-co.

General Form:
(fmt-to-comment-window fmt-string alist col evisc-tuple)
where these arguments are as desribed for fmt1; see fmt.