Major Section: PROGRAMMING
Append, which takes two or more arguments, expects all the
arguments except perhaps the last to be true (null-terminated)
lists.  It returns the result of concatenating all the elements of
all the given lists into a single list.  Actually, in ACL2 append
is a macro that expands into calls of the binary function
binary-append.
Append is a Common Lisp function.  See any Common Lisp
documentation for more information.
 
 