1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
|
<html>
<head><title>ACL2-USER.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ACL2-USER</h2>a package the ACL2 user may prefer
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
This package imports the standard Common Lisp symbols that ACL2
supports and also a few symbols from package <code>"ACL2"</code> 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.
<p>
This package imports the symbols listed in
<code>*common-lisp-symbols-from-main-lisp-package*</code>, which contains
hundreds of CLTL function and macro names including those supported
by ACL2 such as <code><a href="CONS.html">cons</a></code>, <code><a href="CAR.html">car</a></code>, and <code><a href="CDR.html">cdr</a></code>. It also imports the symbols in
<code>*acl2-exports*</code>, which contains a few symbols that are frequently
used while interacting with the ACL2 system, such as <code><a href="IMPLIES.html">implies</a></code>,
<code><a href="DEFTHM.html">defthm</a></code>, and <code><a href="REWRITE.html">rewrite</a></code>. It imports nothing else.<p>
Thus, names such as <code><a href="ALISTP.html">alistp</a></code>, <code><a href="MEMBER-EQUAL.html">member-equal</a></code>, and <code><a href="TYPE-SET.html">type-set</a></code>, which are
defined in the <code>"ACL2"</code> package are not present here. If you find
yourself frequently colliding with names that are defined in
<code>"ACL2"</code> you might consider selecting <code>"ACL2-USER"</code> as your current
package (see <a href="IN-PACKAGE.html">in-package</a>). If you select <code>"ACL2-USER"</code> as the
current package, you may then simply type <code><a href="MEMBER-EQUAL.html">member-equal</a></code> to refer to
<code>acl2-user::member-equal</code>, which you may define as you see fit. Of
course, should you desire to refer to the <code>"ACL2"</code> version of
<code><a href="MEMBER-EQUAL.html">member-equal</a></code>, you will have to use the <code>"ACL2::"</code> prefix, e.g.,
<code>acl2::member-equal</code>.<p>
If, while using <code>"ACL2-USER"</code> as the current package, you find that
there are symbols from <code>"ACL2"</code> 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 <code><a href="UNION-THEORIES.html">union-theories</a></code>
and <code><a href="UNIVERSAL-THEORY.html">universal-theory</a></code> be imported? Except for stabilizing on the
``frequently used'' names from <code>"ACL2"</code>, we intend never to define a
symbol whose <code><a href="SYMBOL-PACKAGE-NAME.html">symbol-package-name</a></code> is <code>"ACL2-USER"</code>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|