How to start using ACL2; the ACL2 command loop
When you start up ACL2, you'll probably find yourself inside the ACL2 command loop, as indicated by the following prompt.
If not, you should type
You should now be in ACL2. The current ``default-defun-mode'' is
ACL2 !>(defun my-cons (x y) (cons x y))
An easy theorem may then be proved: the car of
ACL2 !>(defthm car-my-cons (equal (car (my-cons a b)) a))
You can place raw Lisp forms to evaluate at start-up into file
But be careful; all bets are off when you submit forms to raw Lisp, so this
capability should only be used when you are hacking or when you are setting
some Lisp parameters (e.g.,
Notice that unlike Nqthm, the theorem command is defthm
Various keyword commands are available to query the ACL2 ``world'',
or database. For example, we may view the definition of
ACL2 !>:pe my-cons
Also see pe. We may also view all the lemmas that rewrite
terms whose top function symbol is car by using the following
command, whose output will refer to the lemma
ACL2 !>:pl car
Also see pl. Finally, we may print all the commands back through the initial world as follows.
ACL2 !>:pbt 0
See history for a list of commands, including these, for viewing the current ACL2 world.
Continue with the documentation for annotated-ACL2-scripts to see a simple but illustrative example in the use of ACL2 for reasoning about functions.