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
39
|
<html>
<head><title>UPDATE-NTH.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>UPDATE-NTH</h2>modify a list by putting the given value at the given position
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<code>(Update-nth key val l)</code> returns a list that is the same as the
list <code>l</code>, except that the value at the <code>0</code>-based position <code>key</code>
(a natural number) is <code>val</code>.
<p>
If <code>key</code> is an integer at least as large as the length of <code>l</code>, then
<code>l</code> will be padded with the appropriate number of <code>nil</code> elements,
as illustrated by the following example.
<pre>
ACL2 !>(update-nth 8 'z '(a b c d e))
(A B C D E NIL NIL NIL Z)
</pre>
We have the following theorem.
<pre>
(implies (and (true-listp l)
(integerp key)
(<= 0 key))
(equal (length (update-nth key val l))
(if (< key (length l))
(length l)
(+ 1 key))))
</pre>
<p>
The <a href="GUARD.html">guard</a> of <code>update-nth</code> requires that its first (position)
argument is a natural number and its last (list) argument 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>
|
