## An Example of ACL2 in Use

To introduce you to ACL2 we will consider the `app`

function discussed
in the Common Lisp page, **except** we will omit
for the moment the **declare** form, which in ACL2 is called a **guard**.
We will deal with guards later.
Here is the definition again

**(defun app (x y)**
**(cond ((endp x) y)**
**(t (cons (car x) **
**(app (cdr x) y)))))**

The next few stops along the Walking Tour will show you

* how to use the ACL2 documentation,
* what happens when the above definition is submitted to ACL2,
* what happens when you evaluate calls of `app`

,
* what one simple theorem about `app`

looks like,
* how ACL2 proves the theorem, and
* how that theorem can be used in another proof.

Along the way we will talk about the **definitional principle**, **types**,
the ACL2 **read-eval-print loop**, and how the **theorem prover** works.
When we complete this part of the tour we will introduce the notion of
**guards** and revisit several of the topics above in that context.