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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
<html>
<head><title>TIDBITS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>TIDBITS</h2>some basic hints for using ACL2
<pre>Major Section: <a href="ACL2-TUTORIAL.html">ACL2-TUTORIAL</a>
</pre><p>
<p>
See <a href="BOOKS.html">books</a> for a discussion of books. Briefly, a book is a file
whose name ends in ``.lisp'' that contains ACL2 <a href="EVENTS.html">events</a>;
see <a href="EVENTS.html">events</a>.<p>
See <a href="HISTORY.html">history</a> for a list of useful commands. Some examples:
<pre><p>
:pbt :here ; print the current event
:pbt (:here -3) ; print the last four events
:u ; undo the last event
:pe append ; print the definition of append<p>
</pre>
See <a href="DOCUMENTATION.html">documentation</a> to learn how to print documentation to the
terminal. There are also versions of the <a href="DOCUMENTATION.html">documentation</a> for Mosaic,
Emacs Info, and hardcopy.<p>
There are quite a few kinds of rules allowed in ACL2 besides
<code>:</code><code><a href="REWRITE.html">rewrite</a></code> rules, though we hope that beginners won't usually need
to be aware of them. See <a href="RULE-CLASSES.html">rule-classes</a> for details. In
particular, there is support for <a href="CONGRUENCE.html">congruence</a> rewriting.
See <a href="RUNE.html">rune</a> (``RUle NamE'') for a description of the various kinds
of rules in the system. Also see <a href="THEORIES.html">theories</a> for a description of
how to build <a href="THEORIES.html">theories</a> of <a href="RUNE.html">rune</a>s, which are often used in hints;
see <a href="HINTS.html">hints</a>.<p>
A ``<a href="PROGRAMMING.html">programming</a> mode'' is supported; see <a href="PROGRAM.html">program</a>,
see <a href="DEFUN-MODE.html">defun-mode</a>, and see <a href="DEFAULT-DEFUN-MODE.html">default-defun-mode</a>. It can be
useful to prototype functions after executing the command <code>:</code><code><a href="PROGRAM.html">program</a></code>,
which will cause definitions to be syntaxed-checked only.<p>
ACL2 supports mutual recursion, though this feature is not tied into
the automatic discovery of <a href="INDUCTION.html">induction</a> schemas and is often not the
best way to proceed when you expect to be reasoning about the
functions. See <a href="DEFUNS.html">defuns</a>; also see <a href="MUTUAL-RECURSION.html">mutual-recursion</a>.<p>
See <a href="LD.html">ld</a> for discussion of how to load files of <a href="EVENTS.html">events</a>. There
are many options to <code><a href="LD.html">ld</a></code>, including ones to suppress proofs and to
control output.<p>
The <code>:</code><code><a href="OTF-FLG.html">otf-flg</a></code> (Onward Thru the Fog FLaG) is a useful feature that
Nqthm users have often wished for. It prevents the prover from
aborting a proof attempt and inducting on the original conjecture.
See <a href="OTF-FLG.html">otf-flg</a>.<p>
ACL2 supports redefinition and redundancy in <a href="EVENTS.html">events</a>;
see <a href="LD-REDEFINITION-ACTION.html">ld-redefinition-action</a> and see <a href="REDUNDANT-EVENTS.html">redundant-events</a>.<p>
A <a href="PROOF-TREE.html">proof-tree</a> display feature is available for use with Emacs. This
feature provides a view of ACL2 proofs that can be much more useful
than reading the stream of <a href="CHARACTERS.html">characters</a> output by the theorem prover
as its ``proof.'' See <a href="PROOF-TREE.html">proof-tree</a>.<p>
An interactive feature similar to Pc-Nqthm is supported in ACL2.
See <a href="VERIFY.html">verify</a> and see <a href="PROOF-CHECKER.html">proof-checker</a>.<p>
ACL2 allows you to <a href="MONITOR.html">monitor</a> the use of <a href="REWRITE.html">rewrite</a> rules.
See <a href="BREAK-REWRITE.html">break-rewrite</a>.<p>
See <a href="ARRAYS.html">arrays</a> to read about applicative, fast <a href="ARRAYS.html">arrays</a> in ACL2.<p>
To quit the ACL2 <a href="COMMAND.html">command</a> loop, or (in akcl) to return to the ACL2
<a href="COMMAND.html">command</a> loop after an interrupt, type <code>:</code><code><a href="Q.html">q</a></code>. To continue (resume)
after an interrupt (in akcl), type <code>:r</code>. To cause an interrupt (in
akcl under Unix (trademark of AT&T)), hit control-C (twice, if
inside Emacs). To exit ACL2 altogether, first type <code>:</code><code><a href="Q.html">q</a></code> to exit
the ACL2 <a href="COMMAND.html">command</a> loop, and then exit Lisp (by typing
<code>(user::bye)</code> in akcl).<p>
See <a href="STATE.html">state</a> to read about the von Neumannesque ACL2 <a href="STATE.html">state</a> object that
records the ``current state'' of the ACL2 session.
Also see <a href="_at_.html">@</a>, and see <a href="ASSIGN.html">assign</a>, to learn about reading and
setting global <a href="STATE.html">state</a> variables.<p>
If you want your own von Neumannesque object, e.g., a structure that
can be ``destructively modified'' but which must be used with some
syntactic restrictions, see <a href="STOBJ.html">stobj</a>.
<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>
|
