Evaluating App on Sample Input

ACL2 !>(app nil '(x y z))
(X Y Z)


ACL2 !>(app '(1 2 3) '(4 5 6 7))
(1 2 3 4 5 6 7)


ACL2 !>(app '(a b c d e f g) '(x y z))   ; click here for an explanation
(A B C D E F G X Y Z)


ACL2 !>(app (app '(1 2) '(3 4)) '(5 6))
(1 2 3 4 5 6)


ACL2 !>(app '(1 2) (app '(3 4) '(5 6)))
(1 2 3 4 5 6)


ACL2!>(let ((a '(1 2))
            (b '(3 4))
            (c '(5 6)))
        (equal (app (app a b) c)
               (app a (app b c))))
T

As we can see from these examples, ACL2 functions can be executed more or less as Common Lisp.

The last three examples suggest an interesting property of app.