		Search-engine friendly clone of the ACL2 documentation.

Code-char

The character corresponding to a given numeric code

This function maps a numeric code to the corresponding character, for example: (code-char 65) evaluates to #\A. See char-code for a sort of inverse function, which maps a character to its code.

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.

Subtopics

Code-char-lemmas: Lemmas about code-char from the std/strings library.
Code-char-injectivity-theorem: code-char is injective on natural numbers below 256.
Code-char-inverses-theorems: code-char and char-code are mutual inverses.