Map an array-to-list conversion function to the corresponding Java primitive type.
(atj-jprimarr-conv-tolist-fn-to-ptype fn) → ptype
Function:
(defun atj-jprimarr-conv-tolist-fn-to-ptype (fn) (declare (xargs :guard (atj-jprimarr-conv-tolist-fn-p fn))) (let ((__function__ 'atj-jprimarr-conv-tolist-fn-to-ptype)) (declare (ignorable __function__)) (case fn (boolean-array-to-boolean-list (primitive-type-boolean)) (char-array-to-ubyte16-list (primitive-type-char)) (byte-array-to-sbyte8-list (primitive-type-byte)) (short-array-to-sbyte16-list (primitive-type-short)) (int-array-to-sbyte32-list (primitive-type-int)) (long-array-to-sbyte64-list (primitive-type-long)) (t (prog2$ (impossible) (ec-call (primitive-type-fix :irrelevant)))))))
Theorem:
(defthm primitive-typep-of-atj-jprimarr-conv-tolist-fn-to-ptype (b* ((ptype (atj-jprimarr-conv-tolist-fn-to-ptype fn))) (primitive-typep ptype)) :rule-classes :rewrite)