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 ofAlong the way we will talk about the definitional principle, types, the ACL2 read-eval-print loop, and how the theorem prover works.
app, * what one simple theorem about
applooks like, * how ACL2 proves the theorem, and * how that theorem can be used in another proof.
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.