		Search-engine friendly clone of the ACL2 documentation.

Splitgso-event-generation

Splitgso-gen-everything

Generate all the events.

Signature
(splitgso-gen-everything tunits object-ident filepath? new-object1 new-object2 new-type1 new-type2 split-members const-new) → (mv erp event)
Arguments: tunits — Guard (transunit-ensemblep tunits).; object-ident — Guard (identp object-ident).; filepath? — Guard (c$::filepath-optionp filepath?).; new-object1 — Guard (ident-optionp new-object1).; new-object2 — Guard (ident-optionp new-object2).; new-type1 — Guard (ident-optionp new-type1).; new-type2 — Guard (ident-optionp new-type2).; split-members — Guard (ident-listp split-members).; const-new — Guard (symbolp const-new).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: splitgso-gen-everything

(defun splitgso-gen-everything
       (tunits object-ident filepath?
               new-object1 new-object2 new-type1
               new-type2 split-members const-new)
 (declare (xargs :guard (and (transunit-ensemblep tunits)
                             (identp object-ident)
                             (c$::filepath-optionp filepath?)
                             (ident-optionp new-object1)
                             (ident-optionp new-object2)
                             (ident-optionp new-type1)
                             (ident-optionp new-type2)
                             (ident-listp split-members)
                             (symbolp const-new))))
 (declare (xargs :guard (transunit-ensemble-annop tunits)))
 (let ((__function__ 'splitgso-gen-everything))
   (declare (ignorable __function__))
   (b*
    (((reterr) '(_))
     ((erp tunits)
      (splitgso-transunit-ensemble filepath? object-ident
                                   new-object1 new-object2 new-type1
                                   new-type2 split-members tunits))
     (defconst-event
          (cons 'defconst
                (cons const-new
                      (cons (cons 'quote (cons tunits 'nil))
                            'nil)))))
    (retok defconst-event))))

Theorem: pseudo-event-formp-of-splitgso-gen-everything.event

(defthm pseudo-event-formp-of-splitgso-gen-everything.event
 (b* (((mv acl2::?erp acl2::?event)
       (splitgso-gen-everything tunits object-ident filepath?
                                new-object1 new-object2 new-type1
                                new-type2 split-members const-new)))
   (pseudo-event-formp event))
 :rule-classes :rewrite)