Major Section: ACL2-BUILT-INS
ACL2 accepts 256 distinct characters, which are the characters
obtained by applying the function
code-char to each integer from
255. Among these, Common Lisp designates certain ones as
standard characters, namely those of the form
n is from
126, together with
actual standard characters may be viewed by evaluating the
To be more precise, Common Lisp does not specify the precise
code-char and the standard characters.
However, we check that the underlying Common Lisp implementation
uses a particular relationship that extends the usual ASCII coding
of characters. We also check that Space, Tab, Newline, Page, and
Rubout correspond to characters with respective
char-codes 32, 9,
10, 12, and 127.
Code-char has an inverse,
char-code. Thus, when
applied to an ACL2 character,
c, it returns a number
255 inclusive such that
(code-char n) =
The preceding paragraph implies that there is only one ACL2 character with a given character code. CLTL allows for ``attributes'' for characters, which could allow distinct characters with the same code, but ACL2 does not allow this.
The Character Reader
ACL2 supports the `
#\' notation for characters provided by Common
Lisp, with some restrictions. First of all, for every character
#\cmay be used to denote the character object
c. That is, the user may type in this notation and ACL2 will read it as denoting the character object
c. In this case, the character immediately following
cmust be one of the following ``terminating characters'': a Tab, a Newline, a Page character, a space, or one of the characters:
" ' ( ) ; ` ,Other than the notation above, ACL2 accepts alternate notation for five characters.
#\Space #\Tab #\Newline #\Page #\Rubout
Again, in each of these cases the next character must be from among
the set of ``terminating characters'' described in the
single-character case. Our implementation is consistent with
IS0-8859, even though we don't provide
#\ syntax for entering
characters other than that described above.
Finally, we note that it is our intention that any object printed by ACL2's top-level-loop may be read back into ACL2. Please notify the implementors if you find a counterexample to this claim.