Convert a Java
(byte-array-to-sbyte8-list array) → list
Function:
(defun byte-array-to-sbyte8-list-aux (comps) (declare (xargs :guard (byte-value-listp comps))) (let ((__function__ 'byte-array-to-sbyte8-list-aux)) (declare (ignorable __function__)) (cond ((endp comps) nil) (t (cons (byte-value->int (car comps)) (byte-array-to-sbyte8-list-aux (cdr comps)))))))
Theorem:
(defthm sbyte8-listp-of-byte-array-to-sbyte8-list-aux (b* ((list (byte-array-to-sbyte8-list-aux comps))) (sbyte8-listp list)) :rule-classes :rewrite)
Theorem:
(defthm len-of-byte-array-to-sbyte8-list-aux (b* ((common-lisp::?list (byte-array-to-sbyte8-list-aux comps))) (equal (len list) (len comps))))
Function:
(defun byte-array-to-sbyte8-list (array) (declare (xargs :guard (byte-arrayp array))) (let ((__function__ 'byte-array-to-sbyte8-list)) (declare (ignorable __function__)) (byte-array-to-sbyte8-list-aux (byte-array->components array))))
Theorem:
(defthm sbyte8-listp-of-byte-array-to-sbyte8-list (b* ((list (byte-array-to-sbyte8-list array))) (sbyte8-listp list)) :rule-classes :rewrite)
Theorem:
(defthm len-of-byte-array-to-sbyte8-list (b* ((common-lisp::?list (byte-array-to-sbyte8-list array))) (equal (len list) (len (byte-array->components array)))))