		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Byte-array-new-init

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

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

Definitions and Theorems

Function: byte-array-new-init

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

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

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