other
(in-package "ACL2")
*max-array-maximum-length*constant
(defconst *max-array-maximum-length* (array-maximum-length-bound))
*max-1d-array-length*constant
(defconst *max-1d-array-length* (+ -1 *max-array-maximum-length*))
*max-1d-array-index*constant
(defconst *max-1d-array-index* (+ -1 *max-1d-array-length*))