Major Section: MISCELLANEOUS
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.
