The recognizer of the fixtype of the values of a primitive type.
(primitive-type-predicate type) → predicate
Function:
(defun primitive-type-predicate (type) (declare (xargs :guard (primitive-typep type))) (let ((__function__ 'primitive-type-predicate)) (declare (ignorable __function__)) (packn-pos (list (symbol-name (primitive-type-kind type)) '-valuep) (pkg-witness "JAVA"))))
Theorem:
(defthm symbolp-of-primitive-type-predicate (b* ((predicate (primitive-type-predicate type))) (symbolp predicate)) :rule-classes :rewrite)