		Search-engine friendly clone of the ACL2 documentation.

Append

concatenate zero or more lists

Append, which takes zero or more arguments, expects all the arguments except perhaps the last to be true (nil-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. See append-without-guard for a version of append that has a guard of t.

Macro: append

(defmacro append (&rest rst)
  (cond ((null rst) nil)
        ((null (cdr rst)) (car rst))
        (t (xxxjoin 'binary-append rst))))

Function: binary-append

(defun binary-append (x y)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) y)
        (t (cons (car x)
                 (binary-append (cdr x) y)))))

Subtopics

Std/lists/append: Lemmas about append available in the std/lists library.
Binary-append: concatenate two lists
Append-theorems: Some theorems about the built-in function append.
Append-without-guard: Version of append that has a guard of t
Hons-append: APPEND using HONS instead of CONS