CODE-CHAR.html -- ACL2 Version 3.1

CODE-CHAR

the character corresponding to a given numeric code

Major Section:  PROGRAMMING

Completion Axiom:

(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.