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