ACL2 accepts 256 distinct characters, which are the characters
obtained by applying the function code-char
to each integer from 0 to 255. Among these, Common Lisp designates certain
ones as *standard-characters*, namely those of the form (code-char
n) where n is from 33 to 126, together with #\Newline and
#\Space. The actual standard characters may be viewed by evaluating the
constant expression *standard-chars*.
The standard character constants are written by writing a hash mark
followed by a backslash (#\) followed by the character.
The function characterp
recognizes characters. For more details, See characters .