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.
