		Search-engine friendly clone of the ACL2 documentation.

Split-fn

Split-fn-transunit

Transform a translation unit.

Signature
(split-fn-transunit target-fn new-fn-name tunit split-point) → (mv er new-tunit)
Arguments: target-fn — Guard (identp target-fn).; new-fn-name — Guard (identp new-fn-name).; tunit — Guard (transunitp tunit).; split-point — Guard (natp split-point).
Returns: new-tunit — Type (transunitp new-tunit).

Definitions and Theorems

Function: split-fn-transunit

(defun split-fn-transunit (target-fn new-fn-name tunit split-point)
 (declare (xargs :guard (and (identp target-fn)
                             (identp new-fn-name)
                             (transunitp tunit)
                             (natp split-point))))
 (let ((__function__ 'split-fn-transunit))
   (declare (ignorable __function__))
   (b*
     (((transunit tunit) tunit)
      ((mv er extdecls)
       (split-fn-extdecl-list target-fn
                              new-fn-name tunit.decls split-point)))
     (mv er
         (make-transunit :decls extdecls
                         :info tunit.info)))))

Theorem: transunitp-of-split-fn-transunit.new-tunit

(defthm transunitp-of-split-fn-transunit.new-tunit
  (b* (((mv acl2::?er ?new-tunit)
        (split-fn-transunit target-fn
                            new-fn-name tunit split-point)))
    (transunitp new-tunit))
  :rule-classes :rewrite)