### DIGIT-TO-CHAR

map a digit to a character
Major Section: ACL2-BUILT-INS

Example:
ACL2 !>(digit-to-char 8)
#\8

For an integer `n`

from 0 to 15, `(digit-to-char n)`

is the character
corresponding to `n`

in hex notation, using uppercase letters for digits
exceeding 9. If `n`

is in the appropriate range, that result is of course
also the binary, octal, and decimal digit.
The guard for `digit-to-char`

requires its argument to be an
integer between 0 and 15, inclusive.

To see the ACL2 definition of this function, see pf.