Pretty-print a type.
Function:
(defun print-jtype (type) (declare (xargs :guard (jtypep type))) (let ((__function__ 'print-jtype)) (declare (ignorable __function__)) (jtype-case type :prim (print-primitive-type type.type) :class type.name :array (msg "~@0[]" (print-jtype type.comp)))))
Theorem:
(defthm msgp-of-print-jtype (b* ((part (print-jtype type))) (msgp part)) :rule-classes :rewrite)