		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 const-new) → (mv erp event)
Arguments: filepath — Guard (filepathp filepath).; tunit — Guard (transunitp tunit).; object-ident — Guard (identp object-ident).; 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 const-new)
  (declare (xargs :guard (and (filepathp filepath)
                              (transunitp tunit)
                              (identp object-ident)
                              (symbolp const-new))))
  (declare (ignore filepath tunit object-ident const-new))
  (let ((__function__ 'splitgso-gen-everything))
    (declare (ignorable __function__))
    (b* (((reterr) '(_))) (reterr :todo))))

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 const-new)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)