Major Section: ACL2-BUILT-INS
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
*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
in order to avoid insertion of backslash (\) characters for margins;
also see cw!. Note that even if you change the value of
standard-co (see standard-co),
fmt-to-comment-window will print to
*standard-co*, which is the original value of
General Form: (fmt-to-comment-window fmt-string alist col evisc-tuple)where these arguments are as desribed for
fmt1; see fmt.