The destructor of the fixtype of the values of a primitive type.
(primitive-type-destructor type) → destructor
Function:
(defun primitive-type-destructor (type) (declare (xargs :guard (primitive-typep type))) (let ((__function__ 'primitive-type-destructor)) (declare (ignorable __function__)) (primitive-type-case type :boolean 'boolean-value->bool :char 'char-value->nat :byte 'byte-value->int :short 'short-value->int :int 'int-value->int :long 'long-value->int :float 'float-value->float :double 'double-value->double)))
Theorem:
(defthm symbolp-of-primitive-type-destructor (b* ((destructor (primitive-type-destructor type))) (symbolp destructor)) :rule-classes :rewrite)