Cw-print-base-radix
Print to the comment window in a given print-base
See cw for relevant background. This variant of cw
requires specification of a print-base and, optionally, a print-radix (see
set-print-base, set-print-radix, and set-print-base-radix).
The following examples show that cw-print-base-radix is just like
cw, except that there is a new argument in the first position that
specifies the print-base and can, for that print-base, override the default
print-radix.
ACL2 !>(cw-print-base-radix 16 "~x0~%" '(3 12 16 17))
(#x3 #xC #x10 #x11)
NIL
ACL2 !>(cw-print-base-radix '(16 . t) "~x0~%" '(3 12 16 17))
(#x3 #xC #x10 #x11)
NIL
ACL2 !>(cw-print-base-radix '(16 . nil) "~x0~%" '(3 12 16 17))
(3 C 10 11)
NIL
ACL2 !>(cw-print-base-radix 10 "~x0~%" '(3 12 16 17))
(3 12 16 17)
NIL
ACL2 !>(cw-print-base-radix '(10 . t) "~x0~%" '(3 12 16 17))
(3. 12. 16. 17.)
NIL
ACL2 !>(cw-print-base-radix '(10 . nil) "~x0~%" '(3 12 16 17))
(3 12 16 17)
NIL
ACL2 !>
@({
General Forms:
(cw-print-base-radix print-base fmt-string arg1 arg2 ... argn)
(cw-print-base-radix print-base/print-radix fmt-string arg1 arg2 ... argn)
where all arguments of this macro are evaluated; print-base is a legal
print-base as recognized by print-base-p; print-base/print-radix
is a cons whose car is a legal print-base; fmt-string is a string
suitable for passing to fmt; and arg1 through argn (where n
is at most 9) are corresponding arguments for fmt-string. Printing is
done according to the specified print-base, which is the first argument in the
first general form and is the car of the first argument in the second general
form. The print-radix value that is used for printing in the first general
form is the print-radix as specified for set-print-base-radix, while
in the second general form, it is the cdr.
