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