ACL2-USER

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