		Search-engine friendly clone of the ACL2 documentation.

Aset1-trusted

Set the elements of a 1-dimensional array without invariant-risk

Example Form:
(aset1-trusted 'delta1 a (+ i k) 27)

General Form:
(aset1-trusted name alist index val)

This utility is identical to aset1; in fact, it has the same guard. The difference is that it does not carry invariant-risk. Because of that, functions that call aset1-trusted may suffer from invariant-risk but not be noted by the system as carrying invariant-risk. Therefore, aset1-trusted it is untouchable and should be used with great care. If your system consists of :logic-mode functions, then there is no reason to use aset1-trusted, because only :program-mode functions truly carry invariant-risk.

Function: aset1-trusted

(defun aset1-trusted (name l n val)
  (declare (xargs :guard (and (array1p name l)
                              (integerp n)
                              (>= n 0)
                              (< n (car (dimensions name l))))))
  (aset1 name l n val))