ACL2 !>(app '(a b c) 27) (A B C . 27)illustrates the fact that ACL2's logic is untyped (click here for a brief discussion of the typed versus untyped nature of the logic).
The definition of
app makes no restriction of the arguments to lists.
The definition says that if the first argument satisfies
then return the second argument. In this example, when
app has recursed
three times down the
cdr of its first argument,
'(a b c), it reaches
nil, which satisfies
endp, and so 27 is returned. It is
naturally consed into the emerging list as the function returns from
successive recursive calls (since
cons does not require its arguments to
be lists, either). The result is an ``improper'' list,
(a b c . 27).
You can think of
(app x y) as building a binary tree by replacing the
right-most tip of the tree
x with the tree