		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Char-array-new-init

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

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

Definitions and Theorems

Function: char-array-new-init

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

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

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