Major Section: PROGRAMMING
This package imports the standard Common Lisp symbols that ACL2
supports and also a few symbols from package "ACL2" that are
commonly used when interacting with ACL2. You may prefer to select
this as your current package so as to avoid colliding with ACL2
system names.
This package imports the symbols listed in
*common-lisp-symbols-from-main-lisp-package*, which contains
hundreds of CLTL function and macro names including those supported
by ACL2 such as cons, car, and cdr. It also imports the symbols in
*acl2-exports*, which contains a few symbols that are frequently
used while interacting with the ACL2 system, such as implies,
defthm, and rewrite. It imports nothing else.
Thus, names such as alistp, member-equal, and type-set, which are
defined in the "ACL2" package are not present here. If you find
yourself frequently colliding with names that are defined in
"ACL2" you might consider selecting "ACL2-USER" as your current
package (see in-package). If you select "ACL2-USER" as the
current package, you may then simply type member-equal to refer to
acl2-user::member-equal, which you may define as you see fit. Of
course, should you desire to refer to the "ACL2" version of
member-equal, you will have to use the "ACL2::" prefix, e.g.,
acl2::member-equal.
If, while using "ACL2-USER" as the current package, you find that
there are symbols from "ACL2" that you wish we had imported into
it (because they are frequently used in interaction), please bring
those symbols to our attention. For example, should union-theories
and universal-theory be imported? Except for stabilizing on the
``frequently used'' names from "ACL2", we intend never to define a
symbol whose symbol-package-name is "ACL2-USER".
