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
|
<html>
<head><title>TAKE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>TAKE</h2>initial segment of a list
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
For any natural number <code>n</code> not exceeding the length of <code>l</code>,
<code>(take n l)</code> collects the first <code>n</code> elements of the list <code>l</code>.
<p>
The following is a theorem (though it takes some effort, including
lemmas, to get ACL2 to prove it):
<pre>
(equal (length (take n l)) (nfix n))
</pre>
If <code>n</code> is is an integer greater than the length of <code>l</code>, then
<code>take</code> pads the list with the appropriate number of <code>nil</code>
elements. Thus, the following is also a theorem.
<pre>
(implies (and (integerp n)
(true-listp l)
(<= (length l) n))
(equal (take n l)
(append l (make-list (- n (length l))))))
</pre>
For related functions, see <a href="NTHCDR.html">nthcdr</a> and see <a href="BUTLAST.html">butlast</a>.<p>
The <a href="GUARD.html">guard</a> for <code>(take n l)</code> is that <code>n</code> is a nonnegative integer
and <code>l</code> is a true list.
<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>
|