		Search-engine friendly clone of the ACL2 documentation.

Indnamememo

Get-indname

Read the nth element of the indnamememo array.

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

Function: indnames$ai

(defun
    indnames$ai (stobjs::i indnamememo$a)
    (declare
         (xargs :guard (and (indnamememo$ap indnamememo$a)
                            (integerp stobjs::i)
                            (<= 0 stobjs::i)
                            (< stobjs::i
                               (indnames$a-length indnamememo$a)))))
    (ec-call (maybe-indname-result-fix$inline
                  (ec-call (nth stobjs::i indnamememo$a)))))