Fmx-cw
(fmx-cw str &rest args) => state
Fmx-cw is a variant of cw: both take the same arguments
and have the same behavior on well-formed input, and both return nil.
See cw for documentation on how to use both utilities. Unlike cw,
fmx-cw is well-guarded, so it can catch errors in the use of
tilde-directives. Here is an example of such a guard violation.
ACL2 !>(fmx-cw "Hello ~s0." '(world))
ACL2 Error in TOP-LEVEL: Guard violation for FMX-CW-FN:
Illegal Fmt Syntax. The tilde-s directive at position 6 of the string
below is illegal because its variable evaluated to (WORLD), which is
not a symbol, a string, or a number.
"Hello ~s0."
ACL2 !>
Thus, call fmx-cw instead of cw in the body of :logic mode definition when you want its guard verification to avoid
runtime errors from that call. (While the guard on fmx-cw is likely
complete in practice, this is not an ironclad guarantee. Perhaps, some day,
all formatted printing code will be fully guarded and guard-verified.) Note
that if you call fmx-cw in a definition, the guard proof may benefit from
the lemma, fmx-cw-msg-1-opener, found in community-book
books/system/fmx-cw.lisp.
The variant fmx!-cw avoids the insertion of backslash () characters
when forced to print past the right margin. Thus, use fmx!-cw instead of
fmx-cw if you want the output to be machine-readable.
