Major Section: ACL2-BUILT-INS
Append, which takes zero 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 if there are at least two arguments; if
there is just one argument then the expansion is that argument; and finally,
(append) expands to nil.
Append is a Common Lisp function. See any Common Lisp documentation for
more information.
