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.