		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Long-array-new-init

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

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

Definitions and Theorems

Function: long-array-new-init

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

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

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