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
#\Space. The actual
standard characters may be viewed by evaluating the constant expression
The standard character constants are written by writing a hash mark followed by a backslash (#\) followed by the character.
characterp recognizes characters. For more
details, See characters .