Pretty-print a primitive type.
(print-primitive-type ptype) → part
Function:
(defun print-primitive-type (ptype) (declare (xargs :guard (primitive-typep ptype))) (let ((__function__ 'print-primitive-type)) (declare (ignorable __function__)) (primitive-type-case ptype :boolean "boolean" :char "char" :byte "byte" :short "short" :int "int" :long "long" :float "float" :double "double")))
Theorem:
(defthm msgp-of-print-primitive-type (b* ((part (print-primitive-type ptype))) (msgp part)) :rule-classes :rewrite)