		Search-engine friendly clone of the ACL2 documentation.

Indnamememo

Set-indname

Modify the nth element of the indnamememo array.

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

Function: update-indnames$ai

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