		Search-engine friendly clone of the ACL2 documentation.

Npn4arr

Set-npn4

Modify the nth element of the npn4arr array.

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

Function: update-npn4s$ai

(defun update-npn4s$ai (stobjs::i stobjs::v npn4arr$a)
 (declare
   (xargs
        :guard (and (npn4arr$ap npn4arr$a)
                    (integerp stobjs::i)
                    (<= 0 stobjs::i)
                    (< stobjs::i (npn4s$a-length npn4arr$a))
                    (maybe-npn4-p stobjs::v)
                    (stobjs::typep$ stobjs::v (unsigned-byte 27)))))
 (ec-call (update-nth stobjs::i (maybe-npn4-fix stobjs::v)
                      npn4arr$a)))