		Search-engine friendly clone of the ACL2 documentation.

Concatenate

Concatenate lists or strings together

Examples:
(concatenate 'string "ab" "cd" "ef")     ; equals "abcdef"
(concatenate 'string "ab")               ; equals "ab"
(concatenate 'list '(a b) '(c d) '(e f)) ; equals '(a b c d e f)
(concatenate 'list)                      ; equals nil

General Form:
(concatenate result-type x1 x2 ... xn)

where n >= 0 and either: result-type is 'string and each xi is a string; or result-type is 'list and each xi is a true list. Concatenate simply concatenates its arguments to form the result string or list. Also see append and see string-append. (The latter immediately generates a call to concatenate when applied to strings.)

Note: We do *not* try to comply with the Lisp language's insistence that concatenate copies its arguments. Not only are we in an applicative setting, where this issue shouldn't matter for the logic, but also we do not actually modify the underlying lisp implementation of concatenate; we merely provide a definition for it.

Concatenate is a Common Lisp function. See any Common Lisp documentation for more information.

Macro: concatenate

(defmacro concatenate (result-type &rest sequences)
  (declare (xargs :guard (or (equal result-type ''string)
                             (equal result-type ''list))))
  (cond ((equal result-type ''string)
         (cond ((and sequences (cdr sequences)
                     (null (cddr sequences)))
                (list 'string-append
                      (car sequences)
                      (cadr sequences)))
               (t (list 'string-append-lst
                        (cons 'list sequences)))))
        ((endp sequences) nil)
        (t (cons 'append
                 (append sequences (list nil))))))

Subtopics

Cat: Alternative to concatenate that has a shorter name and may in some cases be more efficient.