		Search-engine friendly clone of the ACL2 documentation.

Lhsarr

Set-lhs

Modify the nth element of the lhsarr array.

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

Function: update-lhss$ai

(defun update-lhss$ai (stobjs::i stobjs::v lhsarr$a)
 (declare
  (xargs :guard (and (lhsarr$ap lhsarr$a)
                     (integerp stobjs::i)
                     (<= 0 stobjs::i)
                     (< stobjs::i (lhss$a-length lhsarr$a))
                     (lhs-p stobjs::v)
                     (stobjs::typep$ stobjs::v (satisfies lhs-p)))))
 (ec-call (update-nth stobjs::i (lhs-fix$inline stobjs::v)
                      lhsarr$a)))