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

ACL2 !>(digit-to-char 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.