		Search-engine friendly clone of the ACL2 documentation.

Split-fn-event-generation

Split-fn-fn

Event expansion of split-fn.

Signature
(split-fn-fn const-old const-new target new-fn split-point 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-fn-fn

(defun split-fn-fn (const-old const-new
                              target new-fn split-point ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (ctxp ctx)))
  (b* (((mv erp event)
        (split-fn-process-inputs-and-gen-everything
             const-old const-new
             target new-fn split-point (w state)))
       ((when erp)
        (er-soft+ ctx t '(_) "~@0" erp)))
    (value event)))

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

(defthm booleanp-of-split-fn-fn.erp
  (b* (((mv acl2::?erp acl2::?event acl2::?state)
        (split-fn-fn const-old const-new
                     target new-fn split-point ctx state)))
    (booleanp erp))
  :rule-classes :type-prescription)

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

(defthm pseudo-event-formp-of-split-fn-fn.event
  (b* (((mv acl2::?erp acl2::?event acl2::?state)
        (split-fn-fn const-old const-new
                     target new-fn split-point ctx state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)