Name of the theorems asserting what value-kind is when the recognizer for a type holds.
(atc-type-to-value-kind-thm type prec-tags) → value-kind-thm
Function:
(defun atc-type-to-value-kind-thm (type prec-tags) (declare (xargs :guard (and (typep type) (atc-string-taginfo-alistp prec-tags)))) (let ((__function__ 'atc-type-to-value-kind-thm)) (declare (ignorable __function__)) (if (or (type-case type :struct) (and (type-case type :pointer) (type-case (type-pointer->to type) :struct))) (defstruct-info->value-kind-thm (atc-tag-info->defstruct (atc-get-tag-info (if (type-case type :struct) (type-struct->tag type) (type-struct->tag (type-pointer->to type))) prec-tags))) (pack 'value-kind-when- (atc-type-to-recognizer type prec-tags)))))
Theorem:
(defthm symbolp-of-atc-type-to-value-kind-thm (b* ((value-kind-thm (atc-type-to-value-kind-thm type prec-tags))) (symbolp value-kind-thm)) :rule-classes :rewrite)