1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
<html>
<head><title>ACL2_Characters.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ACL2 Characters</h2>
<p>
ACL2 accepts 256 distinct characters, which are the characters
obtained by applying the function <code><a href="CODE-CHAR.html">code-char</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> to each
integer from 0 to 255. Among these, Common Lisp designates certain
ones as <code>*standard-characters*</code>, namely those of the form
<code>(code-char n)</code> where n is from 33 to 126, together with
<code>#\Newline</code> and <code>#\Space</code>. The actual standard characters may
be viewed by evaluating the constant expression
<code>*standard-chars*</code>.<p>
The standard character constants are written by writing a hash mark
followed by a backslash (#\) followed by the character.<p>
The function <code><a href="CHARACTERP.html">characterp</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> recognizes characters. For more
details, See <a href="CHARACTERS.html">characters</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
