		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))))
 (let ((__function__ 'copy-fn-fundef))
  (declare (ignorable __function__))
  (b* (((fundef fundef) fundef)
       ((declor fundef.declor) fundef.declor))
   (dirdeclor-case
    fundef.declor.direct :function-params
    (if
     (equal target-fn
            (dirdeclor-get-ident fundef.declor.direct.decl))
     (make-fundef
         :extension fundef.extension
         :spec fundef.spec
         :declor
         (make-declor
              :pointers fundef.declor.pointers
              :direct (make-dirdeclor-function-params
                           :decl (dirdeclor-ident new-fn)
                           :params fundef.declor.direct.params
                           :ellipsis fundef.declor.direct.ellipsis))
         :decls fundef.decls
         :body (rename-fn-stmt fundef.body target-fn new-fn))
     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)