Control radix in which numbers are printed
Also see set-print-base-radix for a nice combined use of
By default, integers and ratios are printed in base 10. ACL2 also supports printing in radix 2, 8, or 16 by calling set-print-base with the desired radix (base).
(set-print-base 10 state) ; Default printing (set-print-base 16 state) ; Print integers and ratios in hex
Here is a sample log.
ACL2 !>(list 25 25/3) (25 25/3) ACL2 !>(set-print-base 16 state) <state> ACL2 !>(list 25 25/3) (19 19/3) ACL2 !>
See set-print-radix for how to print the radix, for example,
printing the decimal number 25 in print-base 16 as ``
Note: ACL2 events and some other top-level commands (for example,
thm, verify, and history commands such as