print to the comment window
Major Section:  PROGRAMMING


(cw "The goal is ~p0 and the alist is ~x1.~%"
    (untranslate term t nil)
Logically, this expression is equivalent to nil. However, it has the effect of first printing to the so-called ``comment window'' the fmt string as indicated. Thus, cw is like fmt (see fmt) except in three important ways. First, it is a :logic mode function. Second, it neither takes nor returns the ACL2 state; logically cw simply returns nil, although it prints to a comment window that just happens to share the terminal screen with the standard character output *standard-co*. Third, its fmt args are positional references, so that for example
(cw "Answers: ~p0 and ~p1" ans1 ans2)
prints in the same manner as:
(fmt "Answers: ~p0 and ~p1" 
     (list (cons #\0 ans1) (cons #\1 ans2))
     *standard-co* state nil)
Typically, calls of cw are embedded in prog2$ forms, e.g.,
(prog2$ (cw ...)
        (mv a b c))
which has the side-effect of printing to the comment window and logically returning (mv a b c).

General Form:
(cw fmt-string arg1 arg2 ... argn)
where n is between 0 and 9 (inclusive). The macro uses fmt-to-comment-window, passing it the column 0 and evisc-tuple nil, after assembling the appropriate alist binding the fmt vars #\0 through #\9; see fmt. If you want
(a) more than 10 vars,
(b) vars other than the digit chars,
(c) a different column, or
(d) a different evisc-tuple,
then call fmt-to-comment-window instead.