FMT-TO-COMMENT-WINDOW

print to the comment window
Major Section:  PROGRAMMING

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 in essence *standard-co* and the ACL2 state is neither an input nor an output.

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