DIGIT-TO-CHAR

map a digit to a character 
Major Section:  PROGRAMMING


Example:
ACL2 !>(digit-to-char 8)
#\8
For an integer n from 0 to 9, (digit-to-char n) is the character corresponding to n in decimal notation.

The guard for digit-to-char requires its argument to be an integer between 0 and 9, inclusive.