		Search-engine friendly clone of the ACL2 documentation.

Truth4arr

Get-truth4

Read the nth element of the truth4arr array.

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

Function: truth4s$ai

(defun truth4s$ai (stobjs::i truth4arr$a)
  (declare (xargs :guard (and (truth4arr$ap truth4arr$a)
                              (integerp stobjs::i)
                              (<= 0 stobjs::i)
                              (< stobjs::i
                                 (truth4s$a-length truth4arr$a)))))
  (ec-call (truth4-fix (ec-call (nth stobjs::i truth4arr$a)))))