ACL2 Symbols
ACL2 Symbols
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 PLUS and SMITH::ABC. All function and variable
names in ACL2 are symbols. When symbols are used as constants they must be
quoted, as in 'PLUS.
The symbol T is commonly used as the Boolean ``true.'' The symbol
NIL is commonly used both as the Boolean ``false'' and as the ``empty
list.'' Despite sometimes being called the ``empty list'' NIL is a
symbol not an ``empty cons.'' Unlike other symbols, T and
NIL may be used as constants without quoting them.
Usually, symbols are written as sequences of alphanumeric characters other
than those denoting numbers. Thus, A12, +1A and 1+ are symbols
but +12 is a number. Roughly speaking, when symbols are read lower case
characters are converted to upper case, so we frequently do not distinguish
ABC from Abc or abc. Click here 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, |Abc| is a symbol whose first character is
capitalized and whose remaining characters are in lower case. |An odd
duck| is a symbol containing two #\Space characters. See any Common Lisp
documentation for the syntactic rules for symbols.
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
symbol-package-name and
see symbol-name .) The symbol SMITH::ABC is said to be in package
"SMITH" and to have the symbol name "ABC". The symbol ABC in package
"SMITH" is generally not equal to the symbol ABC 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
defpkg .) If the current-package is
"SMITH" then SMITH::ABC may be more briefly written as just ABC.
Intern ``creates'' a symbol of a given name in a given
package.
