|
|
|---|
|
|
|
|---|
An Example of ACL2 in Use
To introduce you to ACL2 we will consider the
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
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.