Transform a translation unit ensumble.
(split-fn-transunit-ensemble target-fn new-fn-name tunits split-point) → (mv er new-tunits)
Function:
(defun split-fn-transunit-ensemble (target-fn new-fn-name tunits split-point) (declare (xargs :guard (and (identp target-fn) (identp new-fn-name) (transunit-ensemblep tunits) (natp split-point)))) (let ((__function__ 'split-fn-transunit-ensemble)) (declare (ignorable __function__)) (b* (((transunit-ensemble tunits) tunits) ((mv er map) (split-fn-filepath-transunit-map target-fn new-fn-name tunits.unwrap split-point))) (mv er (transunit-ensemble map)))))
Theorem:
(defthm transunit-ensemblep-of-split-fn-transunit-ensemble.new-tunits (b* (((mv acl2::?er ?new-tunits) (split-fn-transunit-ensemble target-fn new-fn-name tunits split-point))) (transunit-ensemblep new-tunits)) :rule-classes :rewrite)