		Search-engine friendly clone of the ACL2 documentation.

Split-fn-event-generation

Split-fn-gen-everything

Generate all the events.

Signature
(split-fn-gen-everything code const-new target new-fn split-point) → (mv er? event)
Arguments: code — Guard (code-ensemblep code).; const-new — Guard (symbolp const-new).; target — Guard (identp target).; new-fn — Guard (identp new-fn).; split-point — Guard (natp split-point).
Returns: er? — Type (maybe-msgp er?).; event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: split-fn-gen-everything

(defun split-fn-gen-everything
       (code const-new target new-fn split-point)
  (declare (xargs :guard (and (code-ensemblep code)
                              (symbolp const-new)
                              (identp target)
                              (identp new-fn)
                              (natp split-point))))
  (b*
   (((reterr) '(_))
    ((erp code)
     (split-fn-code-ensemble target new-fn code split-point))
    (defconst-event (cons 'defconst
                          (cons const-new
                                (cons (cons 'quote (cons code 'nil))
                                      'nil)))))
   (retok defconst-event)))

Theorem: maybe-msgp-of-split-fn-gen-everything.er?

(defthm maybe-msgp-of-split-fn-gen-everything.er?
  (b*
   (((mv ?er? acl2::?event)
     (split-fn-gen-everything code
                              const-new target new-fn split-point)))
   (maybe-msgp er?))
  :rule-classes :rewrite)

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

(defthm pseudo-event-formp-of-split-fn-gen-everything.event
  (b*
   (((mv ?er? acl2::?event)
     (split-fn-gen-everything code
                              const-new target new-fn split-point)))
   (pseudo-event-formp event))
  :rule-classes :rewrite)