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 reference manual. So follow these links if you
wish, but use your Back Button to return 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.''
