Print to the comment window
(cw "The goal is ~x0 and the alist is ~x1.~%" (untranslate term t nil) unify-subst)
Logically, this expression is equivalent to
(cw "Answers: ~x0 and ~x1" ans1 ans2)
prints in the same manner as:
(fmt "Answers: ~x0 and ~x1" (list (cons #\0 ans1) (cons #\1 ans2)) *standard-co* state nil)
And finally, output from
Typically, calls of
(prog2$ (cw ...) (mv a b c))
which has the side-effect of printing to the comment window and logically
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
(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.
Finally, we discuss another way to create formatted output that also avoids the need to pass in the ACL2 state. The idea is to use wormholes; see wormhole. Below is a function you can write, along with some calls, providing an illustration of this approach.
(defun my-fmt-to-comment-window (str alist) (wormhole 'my-fmt-to-comment-window '(lambda (whs) whs) (list str alist) '(pprogn (fms (car (@ wormhole-input)) (cadr (@ wormhole-input)) *standard-co* state nil) (value :q)) :ld-verbose nil :ld-error-action :return ; harmless return on error :ld-prompt nil)) ; A non-erroneous call: (my-fmt-to-comment-window "Here is ~x0 for your inspection~%" (list (cons #\0 'foo))) ; An error inside the fmt string (unbound fmt var); note that even ; with the error, the wormhole is exited. (my-fmt-to-comment-window "Here is ~x1 for your inspection~%" (list (cons #\0 'foo))) ; A guard violation in the binding; note that even with the error, ; the wormhole is exited. (my-fmt-to-comment-window "Here is ~x0 for your inspection~%" (list (cons #\0 (car 'foo))))