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-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, e.g., #x3A

Also see print-control for other user-settable print controls.

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-print-base has no effect while these forms are being processed.