Check if a Java
(long-array-index-in-range-p array index) → yes/no
Function:
(defun long-array-index-in-range-p (array index) (declare (xargs :guard (and (long-arrayp array) (int-valuep index)))) (let ((__function__ 'long-array-index-in-range-p)) (declare (ignorable __function__)) (integer-range-p 0 (len (long-array->components array)) (int-value->int index))))
Theorem:
(defthm booleanp-of-long-array-index-in-range-p (b* ((yes/no (long-array-index-in-range-p array index))) (booleanp yes/no)) :rule-classes :rewrite)