Names of the theorems for rewriting the pointer type to the struct type to quoted form.
(atc-type-to-pointer-type-to-quoted-thms type prec-tags) → pointer-type-to-quoted-thms
If the type is a pointer to structure type, we return the singleton list of the theorem that rewrites the type to quoted form. Otherwise, we return the empty list.
Function:
(defun atc-type-to-pointer-type-to-quoted-thms (type prec-tags) (declare (xargs :guard (and (typep type) (atc-string-taginfo-alistp prec-tags)))) (let ((__function__ 'atc-type-to-pointer-type-to-quoted-thms)) (declare (ignorable __function__)) (if (and (type-case type :pointer) (type-case (type-pointer->to type) :struct)) (list (defstruct-info->pointer-type-to-quoted-thm (atc-tag-info->defstruct (atc-get-tag-info (type-struct->tag (type-pointer->to type)) prec-tags)))) nil)))
Theorem:
(defthm symbol-listp-of-atc-type-to-pointer-type-to-quoted-thms (b* ((pointer-type-to-quoted-thms (atc-type-to-pointer-type-to-quoted-thms type prec-tags))) (symbol-listp pointer-type-to-quoted-thms)) :rule-classes :rewrite)