Major Section: PROGRAMMING
See cw for an introduction to the comment window and the usual way to print it.
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-tuplewhere these arguments are as desribed for
fmt1; see fmt.