The example

ACL2 !>illustrates the fact that ACL2's logic is untyped (click here for a brief discussion of the typed versus untyped nature of the logic).(app '(a b c) 27)(A B C . 27)

The definition of `app`

makes no restriction of the arguments to lists.
The definition says that if the first argument satisfies `endp`

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
the final `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 `y`

.