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 in essence *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!.
General Form: (fmt-to-comment-window fmt-string alist col evisc-tuple)where these arguments are as desribed for
fmt1
; see fmt.