CODE-CHAR

the character corresponding to a given numeric code
Major Section:  PROGRAMMING

Completion Axiom (completion-of-code-char):

(equal (code-char x)
       (if (and (integerp x)
                (>= x 0)
                (< x 256))
           (code-char x)
         (code-char 0)))

Guard for (code-char x):

(and (integerp x)
     (>= x 0)
     (< x 256))
ACL2 supports 8-bit characters. Inputs not between 0 and 255 are treated as 0.