Major Section: ACL2-TUTORIAL
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:
See documentation to learn how to print documentation to the terminal. There are also versions of the documentation for Mosaic, Emacs Info, and hardcopy.
: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
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;
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
which will cause definitions to be syntaxed-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
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.
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-checker.
ACL2 allows you to monitor the use of rewrite rules. See break-rewrite.
See arrays to read about applicative, fast arrays in ACL2.
To quit the ACL2 command loop, or (in akcl) to return to the ACL2
command loop after an interrupt, type
q. To continue (resume)
after an interrupt (in akcl), type
:r. 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
q to exit
the ACL2 command loop, and then exit Lisp (by typing
(user::bye) in akcl).
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.