		Search-engine friendly clone of the ACL2 documentation.

4vecarr

Get-4vec

Read the nth element of the 4vecarr array.

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

Function: 4vecs$ai

(defun 4vecs$ai (stobjs::i 4vecarr$a)
 (declare
      (xargs :guard (and (4vecarr$ap 4vecarr$a)
                         (integerp stobjs::i)
                         (<= 0 stobjs::i)
                         (< stobjs::i (4vecs$a-length 4vecarr$a)))))
 (ec-call (4vec-fix$inline (ec-call (nth stobjs::i 4vecarr$a)))))