		Search-engine friendly clone of the ACL2 documentation.

Split-gso-implementation

Split-gso-fn

Event expansion of split-gso.

Signature
(split-gso-fn const-old const-new object-name object-filepath new-object1 new-object2 new-type1 new-type2 split-members ctx state) → (mv erp event state)
Arguments: ctx — Guard (ctxp ctx).
Returns: erp — Type (booleanp erp).; event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: split-gso-fn

(defun split-gso-fn (const-old const-new object-name object-filepath
                               new-object1 new-object2 new-type1
                               new-type2 split-members ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (ctxp ctx)))
  (let ((__function__ 'split-gso-fn))
    (declare (ignorable __function__))
    (b* (((mv erp 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 (w state)))
         ((when erp)
          (er-soft+ ctx t '(_) "~@0" erp)))
      (value event))))

Theorem: booleanp-of-split-gso-fn.erp

(defthm booleanp-of-split-gso-fn.erp
  (b* (((mv acl2::?erp acl2::?event acl2::?state)
        (split-gso-fn const-old
                      const-new object-name object-filepath
                      new-object1 new-object2 new-type1
                      new-type2 split-members ctx state)))
    (booleanp erp))
  :rule-classes :type-prescription)

Theorem: pseudo-event-formp-of-split-gso-fn.event

(defthm pseudo-event-formp-of-split-gso-fn.event
  (b* (((mv acl2::?erp acl2::?event acl2::?state)
        (split-gso-fn const-old
                      const-new object-name object-filepath
                      new-object1 new-object2 new-type1
                      new-type2 split-members ctx state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)