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