		Search-engine friendly clone of the ACL2 documentation.

U32arr

Get-u32

Read the nth element of the u32arr array.

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

Function: u32s$ai

(defun u32s$ai (stobjs::i u32arr$a)
  (declare
       (xargs :guard (and (u32arr$ap u32arr$a)
                          (integerp stobjs::i)
                          (<= 0 stobjs::i)
                          (< stobjs::i (u32s$a-length u32arr$a)))))
  (ec-call (nfix (ec-call (nth stobjs::i u32arr$a)))))