TIDBITS

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:

  :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; 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 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 control output.

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-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.