		Search-engine friendly clone of the ACL2 documentation.

Copy-fn

Copy-fn-fundef

Transform a function definition.

Signature
(copy-fn-fundef fundef target-fn new-fn) → fundef?
Arguments: fundef — Guard (fundefp fundef).; target-fn — Guard (identp target-fn).; new-fn — Guard (identp new-fn).
Returns: fundef? — Type (fundef-optionp fundef?).

Definitions and Theorems

Function: copy-fn-fundef

(defun copy-fn-fundef (fundef target-fn new-fn)
 (declare (xargs :guard (and (fundefp fundef)
                             (identp target-fn)
                             (identp new-fn))))
 (declare (xargs :guard (fundef-annop fundef)))
 (let ((__function__ 'copy-fn-fundef))
  (declare (ignorable __function__))
  (b* (((fundef fundef) fundef)
       ((declor fundef.declor) fundef.declor)
       ((fundef-info info) fundef.info))
   (dirdeclor-case
    fundef.declor.direct :function-params
    (if
     (equal target-fn
            (c$::dirdeclor->ident fundef.declor.direct.declor))
     (make-fundef
      :extension fundef.extension
      :spec fundef.spec
      :declor
      (make-declor
           :pointers fundef.declor.pointers
           :direct (make-dirdeclor-function-params
                        :declor (dirdeclor-ident new-fn)
                        :params fundef.declor.direct.params
                        :ellipsis fundef.declor.direct.ellipsis))
      :decls fundef.decls
      :body
      (make-comp-stmt
           :labels (comp-stmt->labels fundef.body)
           :items
           (block-item-list-rename-fn (comp-stmt->items fundef.body)
                                      info.uid new-fn))
      :info fundef.info)
     nil)
    :otherwise nil))))

Theorem: fundef-optionp-of-copy-fn-fundef

(defthm fundef-optionp-of-copy-fn-fundef
  (b* ((fundef? (copy-fn-fundef fundef target-fn new-fn)))
    (fundef-optionp fundef?))
  :rule-classes :rewrite)