Project the return type theorems for structure writers out of a tag information alist.
(atc-string-taginfo-alist-to-writer-return-thms prec-tags) → thms
These are only the writers that represent C code.
For an integer member,
it is the theorem in the
Function:
(defun atc-string-taginfo-alist-to-writer-return-thms-aux (members) (declare (xargs :guard (defstruct-member-info-listp members))) (let ((__function__ 'atc-string-taginfo-alist-to-writer-return-thms-aux)) (declare (ignorable __function__)) (b* (((when (endp members)) nil) (member (car members)) (thm (if (type-integerp (member-type->type (defstruct-member-info->memtype member))) (defstruct-member-info->writer-return-thm member) (defstruct-member-info->writer-element-return-thm member))) (more-thms (atc-string-taginfo-alist-to-writer-return-thms-aux (cdr members)))) (cons thm more-thms))))
Theorem:
(defthm symbol-listp-of-atc-string-taginfo-alist-to-writer-return-thms-aux (b* ((writer-return-thms (atc-string-taginfo-alist-to-writer-return-thms-aux members))) (symbol-listp writer-return-thms)) :rule-classes :rewrite)
Function:
(defun atc-string-taginfo-alist-to-writer-return-thms (prec-tags) (declare (xargs :guard (atc-string-taginfo-alistp prec-tags))) (let ((__function__ 'atc-string-taginfo-alist-to-writer-return-thms)) (declare (ignorable __function__)) (b* (((when (endp prec-tags)) nil) (info (cdar prec-tags)) (thms (atc-string-taginfo-alist-to-writer-return-thms-aux (defstruct-info->members (atc-tag-info->defstruct info)))) (more-thms (atc-string-taginfo-alist-to-writer-return-thms (cdr prec-tags)))) (append thms more-thms))))
Theorem:
(defthm symbol-listp-of-atc-string-taginfo-alist-to-writer-return-thms (b* ((thms (atc-string-taginfo-alist-to-writer-return-thms prec-tags))) (symbol-listp thms)) :rule-classes :rewrite)