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

Guards are arbitrary ACL2 terms that express the ``intended domain'' of
functions. In that sense, guards are akin to type signatures. However,
Common Lisp and ACL2 are untyped programming languages: while the language
supports several different data types and the types of objects can be
determined by predicates at runtime, any type of object may be passed to any
function. Thus, guards are ``extra-logical.'' Recognizing both the
practical and intellectual value of knowing that your functions are applied
to the kinds of objects you intend, ACL2 imposes guards on Common Lisp and
provides a means of proving that functions are used as intended. But the
story is necessarily complicated and we do not recommend it to the new user.
Get used to the fact that any ACL2 function may be applied to any objects and
program accordingly. Read about 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 return briefly to the notion
of **guards** and revisit several of the topics above in that context.