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
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
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 control output.
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 break-rewrite.
See arrays to read about applicative, fast arrays in ACL2.
To quit the ACL2 command loop, or (in gcl) to return to the ACL2
command loop after an interrupt, 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.