1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
<html>
<head><title>ACL2_Symbols.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ACL2 Symbols</h2>
<p>
Common Lisp's symbols are a data type representing words. They are
frequently regarded as atomic objects in the sense that they are not
frequently broken down into their constituents. Often the only
important properties of symbols is that they are not numbers,
characters, strings, or lists and that two symbols are not equal if
they look different (!). Examples of symbols include <code>PLUS</code> and
<code>SMITH::ABC</code>. All function and variable names in ACL2 are symbols.
When symbols are used as constants they must be quoted, as in
<code>'PLUS</code>.<p>
The symbol <code>T</code> is commonly used as the Boolean ``true.'' The
symbol <code>NIL</code> is commonly used both as the Boolean ``false'' and as
the ``empty list.'' Despite sometimes being called the ``empty
list'' <code>NIL</code> is a <b>symbol</B> not an ``empty cons.'' Unlike other
symbols, <code>T</code> and <code>NIL</code> may be used as constants without quoting
them.<p>
Usually, symbols are written as sequences of alphanumeric characters
other than those denoting numbers. Thus, <code>A12</code>, <code>+1A</code> and <code>1+</code>
are symbols but <code>+12</code> is a number. Roughly speaking, when symbols
are read lower case characters are converted to upper case, so we
frequently do not distinguish <code>ABC</code> from <code>Abc</code> or <code>abc</code>.
Click <a href="Conversion.html">here</a> for information about case conversion
when symbols are read. However, any character can be used in a
symbol, but some characters must be ``escaped'' to allow the Lisp
reader to parse the sequence as a symbol. For example, <code>|Abc|</code> is
a symbol whose first character is capitalized and whose remaining
characters are in lower case. <code>|An odd duck|</code> is a symbol
containing two #\Space characters. See any Common Lisp documentation
for the syntactic rules for symbols.<p>
Technically, a symbol is a special kind of pair consisting of a
package name (which is a string) and a symbol name (which is also a
string). (See <a href="SYMBOL-PACKAGE-NAME.html">symbol-package-name</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> and see <a href="SYMBOL-NAME.html">symbol-name</a>
<a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>.) The symbol SMITH::ABC is said to be in package "SMITH"
and to have the symbol name "ABC". The symbol <code>ABC</code> in package
"SMITH" is generally not equal to the symbol <code>ABC</code> in package
"JONES". However, it is possible to ``import'' symbols from one
package into another one, but in ACL2 this can only be done when the
package is created. (See <a href="DEFPKG.html">defpkg</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>.) If the
<code><a href="CURRENT-PACKAGE.html">current-package</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> is "SMITH" then <code>SMITH::ABC</code> may be
more briefly written as just <code>ABC</code>. <code><a href="INTERN.html">Intern</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> ``creates''
a symbol of a given name in a given package.
<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>
|
