		Search-engine friendly clone of the ACL2 documentation.

Split-fn-when-implementation

Transunit-try-split-fn-when

Signature
(transunit-try-split-fn-when tunit triggers transunits) → (mv er? found tunit$)
Arguments: tunit — Guard (transunitp tunit).; triggers — Guard (ident-setp triggers).; transunits — Guard (transunit-ensemblep transunits).
Returns: er? — Type (maybe-msgp er?).; found — Type (booleanp found).; tunit$ — Type (transunitp tunit$).

Definitions and Theorems

Function: transunit-try-split-fn-when

(defun transunit-try-split-fn-when (tunit triggers transunits)
  (declare (xargs :guard (and (transunitp tunit)
                              (ident-setp triggers)
                              (transunit-ensemblep transunits))))
  (b* (((reterr) nil (c$::irr-transunit))
       ((transunit tunit) tunit)
       ((erp found extdecls)
        (ext-declon-list-try-split-fn-when
             tunit.declons triggers transunits)))
    (retok found
           (make-transunit :comment nil
                           :declons extdecls
                           :info tunit.info))))

Theorem: maybe-msgp-of-transunit-try-split-fn-when.er?

(defthm maybe-msgp-of-transunit-try-split-fn-when.er?
  (b* (((mv ?er? ?found ?tunit$)
        (transunit-try-split-fn-when tunit triggers transunits)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: booleanp-of-transunit-try-split-fn-when.found

(defthm booleanp-of-transunit-try-split-fn-when.found
  (b* (((mv ?er? ?found ?tunit$)
        (transunit-try-split-fn-when tunit triggers transunits)))
    (booleanp found))
  :rule-classes :type-prescription)

Theorem: transunitp-of-transunit-try-split-fn-when.tunit$

(defthm transunitp-of-transunit-try-split-fn-when.tunit$
  (b* (((mv ?er? ?found ?tunit$)
        (transunit-try-split-fn-when tunit triggers transunits)))
    (transunitp tunit$))
  :rule-classes :rewrite)