		Search-engine friendly clone of the ACL2 documentation.

Natarr

Set-nat

Modify the nth element of the natarr array.

In the execution this is an array write, but the logical definition is just a thin wrapper for update-nth:

Function: update-nats$ai

(defun
 update-nats$ai
 (stobjs::i stobjs::v natarr$a)
 (declare
      (xargs :guard (and (natarr$ap natarr$a)
                         (integerp stobjs::i)
                         (<= 0 stobjs::i)
                         (< stobjs::i (nats$a-length natarr$a))
                         (natp stobjs::v)
                         (stobjs::typep$ stobjs::v (integer 0 *)))))
 (ec-call (update-nth stobjs::i (nfix stobjs::v)
                      natarr$a)))