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