NAME

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.