Project the valuep theorems out of a tag information alist.
(atc-string-taginfo-alist-to-valuep-thms prec-tags) → thms
Function:
(defun atc-string-taginfo-alist-to-valuep-thms (prec-tags) (declare (xargs :guard (atc-string-taginfo-alistp prec-tags))) (let ((__function__ 'atc-string-taginfo-alist-to-valuep-thms)) (declare (ignorable __function__)) (b* (((when (endp prec-tags)) nil) (info (cdar prec-tags)) (thm (defstruct-info->valuep-thm (atc-tag-info->defstruct info))) (thms (atc-string-taginfo-alist-to-valuep-thms (cdr prec-tags)))) (cons thm thms))))
Theorem:
(defthm symbol-listp-of-atc-string-taginfo-alist-to-valuep-thms (b* ((thms (atc-string-taginfo-alist-to-valuep-thms prec-tags))) (symbol-listp thms)) :rule-classes :rewrite)