Map an ACL2 function that models a Java primitive array creation with length to the Java component type.
(atj-jprimarr-new-len-fn-to-comp-jtype fn) → type
Function:
(defun atj-jprimarr-new-len-fn-to-comp-jtype (fn) (declare (xargs :guard (atj-jprimarr-new-len-fn-p fn))) (let ((__function__ 'atj-jprimarr-new-len-fn-to-comp-jtype)) (declare (ignorable __function__)) (case fn (boolean-array-new-len (jtype-boolean)) (char-array-new-len (jtype-char)) (byte-array-new-len (jtype-byte)) (short-array-new-len (jtype-short)) (int-array-new-len (jtype-int)) (long-array-new-len (jtype-long)) (float-array-new-len (jtype-float)) (double-array-new-len (jtype-double)) (otherwise (prog2$ (impossible) (ec-call (jtype-fix :irrelevant)))))))
Theorem:
(defthm jtypep-of-atj-jprimarr-new-len-fn-to-comp-jtype (b* ((type (atj-jprimarr-new-len-fn-to-comp-jtype fn))) (jtypep type)) :rule-classes :rewrite)