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