		Search-engine friendly clone of the ACL2 documentation.

Copy-fn

Rename-fn-extdecl

Signature
(rename-fn-extdecl extdecl old-fn new-fn) → new-extdecl
Arguments: extdecl — Guard (extdeclp extdecl).; old-fn — Guard (identp old-fn).; new-fn — Guard (identp new-fn).
Returns: new-extdecl — Type (extdeclp new-extdecl).

Definitions and Theorems

Function: rename-fn-extdecl

(defun rename-fn-extdecl (extdecl old-fn new-fn)
 (declare (xargs :guard (and (extdeclp extdecl)
                             (identp old-fn)
                             (identp new-fn))))
 (declare (ignorable extdecl old-fn new-fn))
 (let ((__function__ 'rename-fn-extdecl))
  (declare (ignorable __function__))
  (extdecl-case
    extdecl
    :fundef
    (extdecl-fundef (rename-fn-fundef extdecl.unwrap old-fn new-fn))
    :decl
    (extdecl-decl (rename-fn-decl extdecl.unwrap old-fn new-fn))
    :empty (extdecl-empty)
    :asm (extdecl-fix extdecl))))

Theorem: extdeclp-of-rename-fn-extdecl

(defthm extdeclp-of-rename-fn-extdecl
  (b* ((new-extdecl (rename-fn-extdecl extdecl old-fn new-fn)))
    (extdeclp new-extdecl))
  :rule-classes :rewrite)