Fmt-to-comment-window
Print to the comment window
General Form:
(fmt-to-comment-window fmt-string alist col evisc-tuple print-base-radix)
where these arguments are as described for fmt1 (see fmt)
except that the last argument is as described for cw-print-base-radix.
See cw for important background. Calls of the macro cw expand
to calls of the function fmt-to-comment-window whose final three
arguments are 0, nil, and nil. For variants of
fmt-to-comment-window that provide readable output (suffix "!")
and are never inhibited (suffix "+"), see fmt-to-comment-window!, fmt-to-comment-window+, and fmt-to-comment-window!+.
Function fmt-to-comment-window is similar to fmt1 (see fmt), except that the channel is *standard-co* and the ACL2 state is neither an input nor an output, and moreover, an additional argument
specifies the print-base and optionally the print-radix. That additional
argument is treated the same as the first argument of
cw-print-base-radix; see cw-print-base-radix. 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!, a macro that expands to a call of
fmt-to-comment-window!. 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.
