Major Section: ACL2-BUILT-INS
(Update-nth key val l) returns a list that is the same as the
l, except that the value at the
(a natural number) is
key is an integer at least as large as the length of
l will be padded with the appropriate number of
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
To see the ACL2 definition of this function, see pf.