Update-nth
Modify a list by putting the given value at the given position
(Update-nth key val l) returns a list that is the same as the
list l, except that the value at the 0-based position key
(a natural number) is val.
If key is an integer at least as large as the length of l, then
l will be padded with the appropriate number of nil elements, as
illustrated by the following example.
ACL2 !>(update-nth 8 'z '(a b c d e))
(A B C D E NIL NIL NIL Z)
We have the following theorem.
(implies (and (true-listp l)
(integerp key)
(<= 0 key))
(equal (length (update-nth key val l))
(if (< key (length l))
(length l)
(+ 1 key))))
The guard of update-nth requires that its first (position)
argument is a natural number and its last (list) argument is a true list.
Function: update-nth
(defun update-nth (key val l)
(declare (xargs :guard (true-listp l))
(type (integer 0 *) key))
(cond ((zp key) (cons val (cdr l)))
(t (cons (car l)
(update-nth (1- key) val (cdr l))))))Subtopics
- Std/lists/update-nth
- Lemmas about update-nth available in the std/lists
library.
- Nth-aliases-table
- A table used to associate names for nth/update-nth printing
