1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
<html>
<head><title>CONCATENATE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>CONCATENATE</h2>concatenate lists or strings together
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<pre>
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
<p>
General Form:
(concatenate result-type x1 x2 ... xn)
</pre>
where <code>n >= 0</code> and either: <code>result-type</code> is <code>'</code><code><a href="STRING.html">string</a></code> and each <code>xi</code> is a
string; or <code>result-type</code> is <code>'</code><code><a href="LIST.html">list</a></code> and each <code>xi</code> is a true list.
<code>Concatenate</code> simply concatenates its arguments to form the result
string or list. Also see <a href="APPEND.html">append</a> and see <a href="STRING-APPEND.html">string-append</a>,
though <code>concatenate</code> is probably preferable to <code><a href="STRING-APPEND.html">string-append</a></code> for
efficiency.<p>
Note: We do *not* try to comply with the Lisp language's insistence
that <code>concatenate</code> 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 <code>concatenate</code>; we merely provide a definition for
it.<p>
<code>Concatenate</code> is a Common Lisp function. See any Common Lisp
documentation for more information.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
