A package the ACL2 user may prefer
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.,
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".