		Search-engine friendly clone of the ACL2 documentation.

Atj-java-primitive-array-model

Long-array-from-sbyte64-list

Convert an ACL2 list of signed 64-bit integers to a Java boolean array.

Signature
(long-array-from-sbyte64-list list) → array
Arguments: list — Guard (sbyte64-listp list).
Returns: array — Type (long-arrayp array).

Definitions and Theorems

Function: long-array-from-sbyte64-list-aux

(defun long-array-from-sbyte64-list-aux (list)
 (declare (xargs :guard (sbyte64-listp list)))
 (let ((__function__ 'long-array-from-sbyte64-list-aux))
   (declare (ignorable __function__))
   (cond ((endp list) nil)
         (t (cons (long-value (car list))
                  (long-array-from-sbyte64-list-aux (cdr list)))))))

Theorem: long-value-listp-of-long-array-from-sbyte64-list-aux

(defthm long-value-listp-of-long-array-from-sbyte64-list-aux
  (b* ((comps (long-array-from-sbyte64-list-aux list)))
    (long-value-listp comps))
  :rule-classes :rewrite)

Theorem: len-of-long-array-from-sbyte64-list-aux

(defthm len-of-long-array-from-sbyte64-list-aux
  (b* ((?comps (long-array-from-sbyte64-list-aux list)))
    (equal (len comps) (len list))))

Function: long-array-from-sbyte64-list

(defun long-array-from-sbyte64-list (list)
  (declare (xargs :guard (sbyte64-listp list)))
  (declare (xargs :guard (< (len list) (expt 2 31))))
  (let ((__function__ 'long-array-from-sbyte64-list))
    (declare (ignorable __function__))
    (long-array (long-array-from-sbyte64-list-aux list))))

Theorem: long-arrayp-of-long-array-from-sbyte64-list

(defthm long-arrayp-of-long-array-from-sbyte64-list
  (b* ((array (long-array-from-sbyte64-list list)))
    (long-arrayp array))
  :rule-classes :rewrite)