thm, verify, and history commands such as :pe and
:pbt) set the print base to 10 during their evaluation. So
set-acl2-print-base has no effect while these forms are being
processed.
Major Section: IO
By default, integers and ratios are printed in base 10. ACL2 also supports printing in radix 2, 8, or 16 by calling set-acl2-print-base with the desired radix (base).
:set-acl2-print-base 10 ; Default printing (set-acl2-print-base 10) ; Same as above :set-acl2-print-base 16 ; Print integers and ratios in hex, e.g., #x3A (set-acl2-print-base 16) ; Same as above
Note: ACL2 events and some other top-level commands (for example,
thm, verify, and history commands such as :pe and
:pbt) set the print base to 10 during their evaluation. So
set-acl2-print-base has no effect while these forms are being
processed.