### SET-ACL2-PRINT-BASE

control radix in which number are printed
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.