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