		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Short-array-new-init

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

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

Definitions and Theorems

Function: short-array-new-init

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

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

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