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