		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Int-array-new-init

Construct a Java int array with the given initializer (i.e. components).

Signature
(int-array-new-init comps) → array
Arguments: comps — Guard (int-value-listp comps).
Returns: array — Type (int-arrayp array).

Definitions and Theorems

Function: int-array-new-init

(defun int-array-new-init (comps)
  (declare (xargs :guard (int-value-listp comps)))
  (declare (xargs :guard (< (len comps) (expt 2 31))))
  (let ((__function__ 'int-array-new-init))
    (declare (ignorable __function__))
    (int-array comps)))

Theorem: int-arrayp-of-int-array-new-init

(defthm int-arrayp-of-int-array-new-init
  (b* ((array (int-array-new-init comps)))
    (int-arrayp array))
  :rule-classes :rewrite)