app again, with the documented topics highlighted. 
All of the
links below lead into the ACL2 online documentation, 1.5 megabytes of
hyperlinked text. So follow these links around, but remember to come
back here!
Most ACL2 primitives are documented. Here is the definition of
app again, with the documented topics highlighted. All of the
links below lead into the ACL2 online documentation, 1.5 megabytes of
hyperlinked text. So follow these links around, but remember to come
back here!
(defun app (x y)
(cond ((endp x) y)
(t (cons (car x)
(app (cdr x) y)))))
By following the link on endp we see that it is a
Common Lisp function and is defined to be the same as atom
, which recognizes non-conses. But endp has a guard.
Since we are ignorning guards for now, we'll ignore the guard issue
on endp.
So this definition reads ``to app x and y: if x is an
atom, return y; otherwise, app (cdr x) and y and then
cons (car x) onto that.''
