CODE-CHAR.html -- ACL2 Version 6.2

CODE-CHAR

the character corresponding to a given numeric code

Major Section:  ACL2-BUILT-INS

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.