Name
Syntactic rules on logical names
Examples Counter-Examples
PRIMEP 91 (not a symbolp)
F-AC-23 :CHK-LIST (in KEYWORD package)
1AX *PACKAGE* (in the Lisp Package)
|Prime Number| 1E3 (not a symbolp)
Many different ACL2 entities have names, e.g., functions, macros,
variables, constants, packages, theorems, theories, etc. Package names
are strings. All other names are symbols and may not be in the
"KEYWORD" package. Moreover, names of functions, macros, constrained
functions, and constants, other than those that are predefined, must not be in
the ``main Lisp package'' (which is ("LISP" or "COMMON-LISP",
according to whether we are following CLTL1 or CLTL2). An analogous
restriction on variables is given below.
T, nil, and all names above except those that begin with
ampersand (&) are names of variables or constants. T, nil, and
those names beginning and ending with star (*) are constants. All other such
names are variables.
Note that names that start with ampersand, such as &rest, may be
lambda list keywords and are reserved for such use whether or not they are in
the CLTL constant lambda-list-keywords. (See pg 82 of CLTL2.) That is,
these may not be used as variables. Unlike constants, variables may be in the
main Lisp package as long as they are in the original list of imports from
that package to ACL2, the list
*common-lisp-symbols-from-main-lisp-package*, and do not belong to a list
of symbols that are potentially ``global.'' This latter list is the value of
*common-lisp-specials-and-constants*.
Our restrictions pertaining to the main Lisp package take into account that
some symbols, e.g., lambda-list-keywords and boole-c2, are
``special.'' Permitting them to be bound could have harmful effects. In
addition, the Common Lisp language does not allow certain manipulations with
many symbols of that package. So, we stay away from them, except for allowing
certain variables as indicated above.
