		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-info->writer-list-aux

Signature
(defstruct-info->writer-list-aux members) → writer-list
Arguments: members — Guard (defstruct-member-info-listp members).
Returns: writer-list — Type (symbol-listp writer-list).

Definitions and Theorems

Function: defstruct-info->writer-list-aux

(defun defstruct-info->writer-list-aux (members)
 (declare (xargs :guard (defstruct-member-info-listp members)))
 (let ((__function__ 'defstruct-info->writer-list-aux))
  (declare (ignorable __function__))
  (cond
       ((endp members) nil)
       (t (cons (defstruct-member-info->writer (car members))
                (defstruct-info->writer-list-aux (cdr members)))))))

Theorem: symbol-listp-of-defstruct-info->writer-list-aux

(defthm symbol-listp-of-defstruct-info->writer-list-aux
  (b* ((writer-list (defstruct-info->writer-list-aux members)))
    (symbol-listp writer-list))
  :rule-classes :rewrite)