Some basic hints for using ACL2
See books for a discussion of books. Briefly, a book is a
file whose name ends in ``.lisp'' that contains ACL2 events; see events.
See history for a list of useful commands. Some examples:
: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
See documentation to learn how to print documentation to the
terminal. There are also versions of the documentation for web
browsers and for Emacs (see ACL2-Doc).
There are quite a few kinds of rules allowed in ACL2 besides :rewrite rules, though we hope that beginners won't usually need to be aware
of them. See rule-classes for details. In particular, there is
support for congruence rewriting. See rune (``RUle NamE'') for
a description of the various kinds of rules in the system. Also see theories for a description of how to build theories of runes,
which are often used in hints; see hints.
A ``programming mode'' is supported; see program, see defun-mode, and see default-defun-mode. It can be useful to prototype
functions after executing the command :program, which will cause
definitions to be syntax-checked only.
ACL2 supports mutual recursion, though this feature is not tied into the
automatic discovery of induction schemas and is often not the best way
to proceed when you expect to be reasoning about the functions. See defuns; also see mutual-recursion.
See ld for discussion of how to load files of events. There
are many options to ld, including ones to suppress proofs and to
The :otf-flg (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 otf-flg.
ACL2 supports redefinition and redundancy in events; see ld-redefinition-action and see redundant-events.
A proof-tree 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 characters output by the theorem prover as its
``proof.'' See proof-tree.
An interactive feature similar to Pc-Nqthm is supported in ACL2. See verify and see proof-builder.
ACL2 allows you to monitor the use of rewrite rules. See
See arrays to read about applicative, fast arrays in
To quit the ACL2 command loop, or (in gcl) to return to the ACL2
command loop after an interrupt, type :q. To continue
(resume) after an interrupt (in gcl), type :r. To cause an interrupt hit
control-C (twice, if inside Emacs). To exit ACL2 altogether, type
See state to read about the von Neumannesque ACL2 state
object that records the ``current state'' of the ACL2 session. Also see @, and see assign, to learn about reading and setting global state variables.
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 stobj.