		Search-engine friendly clone of the ACL2 documentation.

Splitgso-event-generation

Splitgso-gen-everything

Generate all the events.

Signature
(splitgso-gen-everything filepath tunit object-ident new-object1 new-object2 new-type1 new-type2 split-members const-new) → (mv erp event)
Arguments: filepath — Guard (filepathp filepath).; tunit — Guard (transunitp tunit).; object-ident — Guard (identp object-ident).; new-object1 — Guard (identp new-object1).; new-object2 — Guard (identp new-object2).; new-type1 — Guard (identp new-type1).; new-type2 — Guard (identp 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
       (filepath tunit object-ident
                 new-object1 new-object2 new-type1
                 new-type2 split-members const-new)
 (declare (xargs :guard (and (filepathp filepath)
                             (transunitp tunit)
                             (identp object-ident)
                             (identp new-object1)
                             (identp new-object2)
                             (identp new-type1)
                             (identp new-type2)
                             (ident-listp split-members)
                             (symbolp const-new))))
 (let ((__function__ 'splitgso-gen-everything))
  (declare (ignorable __function__))
  (b*
   (((reterr) '(_))
    ((erp tunit)
     (splitgso-transunit object-ident
                         new-object1 new-object2 new-type1
                         new-type2 split-members tunit))
    (defconst-event
     (cons
      'defconst
      (cons
       const-new
       (cons
        (cons
             'transunit-ensemble
             (cons (cons 'omap::update
                         (cons (cons 'quote (cons filepath 'nil))
                               (cons (cons 'quote (cons tunit 'nil))
                                     '(nil))))
                   '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 filepath tunit object-ident
                                new-object1 new-object2 new-type1
                                new-type2 split-members const-new)))
   (pseudo-event-formp event))
 :rule-classes :rewrite)