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