File: ACL2-USER.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (42 lines) | stat: -rw-r--r-- 2,923 bytes parent folder | download
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>