		Search-engine friendly clone of the ACL2 documentation.

Split-gso-implementation

Split-gso-process-inputs-and-gen-everything

Process the inputs and generate the events.

Signature
(split-gso-process-inputs-and-gen-everything const-old const-new object-name object-filepath new-object1 new-object2 new-type1 new-type2 split-members wrld) → (mv er? event)
Arguments: wrld — Guard (plist-worldp wrld).
Returns: er? — Type (maybe-msgp er?).; event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: split-gso-process-inputs-and-gen-everything

(defun split-gso-process-inputs-and-gen-everything
       (const-old const-new object-name
                  object-filepath new-object1 new-object2
                  new-type1 new-type2 split-members wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'split-gso-process-inputs-and-gen-everything))
   (declare (ignorable __function__))
   (b*
    (((reterr) '(_))
     ((erp code object-ident filepath?
           new-object1 new-object2 new-type1
           new-type2 split-members const-new)
      (split-gso-process-inputs
           const-old const-new object-name
           object-filepath new-object1 new-object2
           new-type1 new-type2 split-members wrld))
     ((erp event)
      (split-gso-gen-everything code object-ident filepath?
                                new-object1 new-object2 new-type1
                                new-type2 split-members const-new)))
    (retok event))))

Theorem: maybe-msgp-of-split-gso-process-inputs-and-gen-everything.er?

(defthm
      maybe-msgp-of-split-gso-process-inputs-and-gen-everything.er?
  (b* (((mv ?er? acl2::?event)
        (split-gso-process-inputs-and-gen-everything
             const-old
             const-new object-name object-filepath
             new-object1 new-object2 new-type1
             new-type2 split-members wrld)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-split-gso-process-inputs-and-gen-everything.event

(defthm
 pseudo-event-formp-of-split-gso-process-inputs-and-gen-everything.event
 (b* (((mv ?er? acl2::?event)
       (split-gso-process-inputs-and-gen-everything
            const-old
            const-new object-name object-filepath
            new-object1 new-object2 new-type1
            new-type2 split-members wrld)))
   (pseudo-event-formp event))
 :rule-classes :rewrite)