		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-fn

Process the inputs and generate the events.

Signature
(defstruct-fn args call ctx state) → (mv erp event state)
Arguments: args — Guard (true-listp args).; call — Guard (pseudo-event-formp call).; ctx — Guard (ctxp ctx).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: defstruct-fn

(defun defstruct-fn (args call ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (true-listp args)
                              (pseudo-event-formp call)
                              (ctxp ctx))))
  (let ((__function__ 'defstruct-fn))
    (declare (ignorable __function__))
    (b* (((er (list tag
                    tag-ident members flexiblep redundant)
              :iferr '(_))
          (defstruct-process-inputs args call ctx state))
         ((when redundant)
          (acl2::value '(value-triple :redundant)))
         (event (defstruct-gen-everything
                     tag tag-ident members flexiblep call)))
      (acl2::value event))))

Theorem: pseudo-event-formp-of-defstruct-fn.event

(defthm pseudo-event-formp-of-defstruct-fn.event
  (b* (((mv acl2::?erp acl2::?event acl2::?state)
        (defstruct-fn args call ctx state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)