Build the Java primitive type
(jtype-byte) → type
Function:
(defun jtype-byte nil (declare (xargs :guard t)) (let ((__function__ 'jtype-byte)) (declare (ignorable __function__)) (jtype-prim (primitive-type-byte))))
Theorem:
(defthm jtypep-of-jtype-byte (b* ((type (jtype-byte))) (jtypep type)) :rule-classes :rewrite)