Collect all the
(defstruct-info->writer-element-list info) → writer-list
Function:
(defun defstruct-info->writer-element-list-aux (members) (declare (xargs :guard (defstruct-member-info-listp members))) (let ((__function__ 'defstruct-info->writer-element-list-aux)) (declare (ignorable __function__)) (cond ((endp members) nil) (t (cons (defstruct-member-info->writer-element (car members)) (defstruct-info->writer-element-list-aux (cdr members)))))))
Theorem:
(defthm symbol-listp-of-defstruct-info->writer-element-list-aux (b* ((writer-element-list (defstruct-info->writer-element-list-aux members))) (symbol-listp writer-element-list)) :rule-classes :rewrite)
Function:
(defun defstruct-info->writer-element-list (info) (declare (xargs :guard (defstruct-infop info))) (let ((__function__ 'defstruct-info->writer-element-list)) (declare (ignorable __function__)) (defstruct-info->writer-element-list-aux (defstruct-info->members info))))
Theorem:
(defthm symbol-listp-of-defstruct-info->writer-element-list (b* ((writer-list (defstruct-info->writer-element-list info))) (symbol-listp writer-list)) :rule-classes :rewrite)