		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-gen-all-member-ops

Generate the operations for all the members of the structures defined by the defstruct.

Signature
(defstruct-gen-all-member-ops struct-tag struct-tag-p struct-tag-fix value-kind-when-struct-tag-p valuep-when-struct-tag-p members) → (mv events infos)
Arguments: struct-tag — Guard (symbolp struct-tag).; struct-tag-p — Guard (symbolp struct-tag-p).; struct-tag-fix — Guard (symbolp struct-tag-fix).; value-kind-when-struct-tag-p — Guard (symbolp value-kind-when-struct-tag-p).; valuep-when-struct-tag-p — Guard (symbolp valuep-when-struct-tag-p).; members — Guard (member-type-listp members).
Returns: events — Type (pseudo-event-form-listp events).; infos — Type (defstruct-member-info-listp infos).

Definitions and Theorems

Function: defstruct-gen-all-member-ops

(defun defstruct-gen-all-member-ops
       (struct-tag struct-tag-p struct-tag-fix
                   value-kind-when-struct-tag-p
                   valuep-when-struct-tag-p members)
  (declare (xargs :guard (and (symbolp struct-tag)
                              (symbolp struct-tag-p)
                              (symbolp struct-tag-fix)
                              (symbolp value-kind-when-struct-tag-p)
                              (symbolp valuep-when-struct-tag-p)
                              (member-type-listp members))))
  (let ((__function__ 'defstruct-gen-all-member-ops))
    (declare (ignorable __function__))
    (b* (((when (endp members)) (mv nil nil))
         ((mv event info)
          (defstruct-gen-member-ops
               struct-tag struct-tag-p struct-tag-fix
               value-kind-when-struct-tag-p
               valuep-when-struct-tag-p (car members)))
         ((mv events infos)
          (defstruct-gen-all-member-ops
               struct-tag struct-tag-p struct-tag-fix
               value-kind-when-struct-tag-p
               valuep-when-struct-tag-p
               (cdr members))))
      (mv (cons event events)
          (cons info infos)))))

Theorem: pseudo-event-form-listp-of-defstruct-gen-all-member-ops.events

(defthm
     pseudo-event-form-listp-of-defstruct-gen-all-member-ops.events
  (b* (((mv ?events ?infos)
        (defstruct-gen-all-member-ops
             struct-tag struct-tag-p struct-tag-fix
             value-kind-when-struct-tag-p
             valuep-when-struct-tag-p members)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: defstruct-member-info-listp-of-defstruct-gen-all-member-ops.infos

(defthm
  defstruct-member-info-listp-of-defstruct-gen-all-member-ops.infos
  (b* (((mv ?events ?infos)
        (defstruct-gen-all-member-ops
             struct-tag struct-tag-p struct-tag-fix
             value-kind-when-struct-tag-p
             valuep-when-struct-tag-p members)))
    (defstruct-member-info-listp infos))
  :rule-classes :rewrite)