digit-to-char requires its argument to be an
integer between 0 and 15, inclusive.
Major Section: PROGRAMMING
Example: ACL2 !>(digit-to-char 8) #\8For 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.