CONCATENATE

concatenate lists or strings together
Major Section:  ACL2-BUILT-INS

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.