Convert an ACL2 list of unsigned 16-bit integers to a Java
(char-array-from-ubyte16-list list) → array
Function:
(defun char-array-from-ubyte16-list-aux (list) (declare (xargs :guard (ubyte16-listp list))) (let ((__function__ 'char-array-from-ubyte16-list-aux)) (declare (ignorable __function__)) (cond ((endp list) nil) (t (cons (char-value (car list)) (char-array-from-ubyte16-list-aux (cdr list)))))))
Theorem:
(defthm char-value-listp-of-char-array-from-ubyte16-list-aux (b* ((comps (char-array-from-ubyte16-list-aux list))) (char-value-listp comps)) :rule-classes :rewrite)
Theorem:
(defthm len-of-char-array-from-ubyte16-list-aux (b* ((?comps (char-array-from-ubyte16-list-aux list))) (equal (len comps) (len list))))
Function:
(defun char-array-from-ubyte16-list (list) (declare (xargs :guard (ubyte16-listp list))) (declare (xargs :guard (< (len list) (expt 2 31)))) (let ((__function__ 'char-array-from-ubyte16-list)) (declare (ignorable __function__)) (char-array (char-array-from-ubyte16-list-aux list))))
Theorem:
(defthm char-arrayp-of-char-array-from-ubyte16-list (b* ((array (char-array-from-ubyte16-list list))) (char-arrayp array)) :rule-classes :rewrite)