Major Section: ACL2-TUTORIAL

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 typeACL2 !>

`(LP)`

. See lp, which has a lot more
information about the ACL2 command loop.
You should now be in ACL2. The current ``default-defun-mode'' is
`:`

`logic`

; the other mode is `:`

`program`

, which would cause the letter `p`

to be printed in the prompt. `:`

`Logic`

means that any function we
define is not only executable but also is axiomatically defined in
the ACL2 logic. See defun-mode and
see default-defun-mode. For example we can define a function
`my-cons`

as follows. (You may find it useful to start up ACL2 and
submit this and other commands below to the ACL2 command loop, as we
won't include output below.)

An easy theorem may then be proved: theACL2 !>(defun my-cons (x y) (cons x y))

`car`

of `(my-cons a b)`

is
A.
Notice that unlike Nqthm, the theorem command isACL2 !>(defthm car-my-cons (equal (car (my-cons a b)) a))

`defthm`

rather than
`prove-lemma`

. See defthm, which explains (among other things)
that the default is to turn theorems into rewrite rules.
Various keyword commands are available to query the ACL2 ``world'',
or database. For example, we may view the definition of `my-cons`

by
invoking a command to print events, as follows.

Also see pe. We may also view all the lemmas that rewrite terms whose top function symbol isACL2 !>:pe my-cons

`car`

by using the following
command, whose output will refer to the lemma `car-my-cons`

proved
above.
Also see pl. Finally, we may print all the commands back through the initial world as follows.ACL2 !>:pl car

See history for a list of commands, including these, for viewing the current ACL2 world.ACL2 !>:pbt 0

Continue with the documentation for tutorial-examples to
see a simple but illustrative example in the use of ACL2 for
reasoning about functions.