Map an ACL2 function that models a Java primitive array constructor with initializer to the corresponding primitive type.
(atj-jprimarr-new-init-fn-to-ptype fn) → ptype
Function:
(defun atj-jprimarr-new-init-fn-to-ptype (fn) (declare (xargs :guard (atj-jprimarr-new-init-fn-p fn))) (let ((__function__ 'atj-jprimarr-new-init-fn-to-ptype)) (declare (ignorable __function__)) (case fn (boolean-array-new-init (primitive-type-boolean)) (char-array-new-init (primitive-type-char)) (byte-array-new-init (primitive-type-byte)) (short-array-new-init (primitive-type-short)) (int-array-new-init (primitive-type-int)) (long-array-new-init (primitive-type-long)) (t (prog2$ (impossible) (ec-call (primitive-type-fix :irrelevant)))))))
Theorem:
(defthm primitive-typep-of-atj-jprimarr-new-init-fn-to-ptype (b* ((ptype (atj-jprimarr-new-init-fn-to-ptype fn))) (primitive-typep ptype)) :rule-classes :rewrite)