		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Fundef-rename-fn

Signature
(fundef-rename-fn fundef uid new-fn) → fty::result
Arguments: fundef — Guard (fundefp fundef).; uid — Guard (c$::uidp uid).; new-fn — Guard (identp new-fn).
Returns: fty::result — Type (fundefp fty::result).

Definitions and Theorems

Function: fundef-rename-fn

(defun fundef-rename-fn (fundef uid new-fn)
  (declare (xargs :guard (and (fundefp fundef)
                              (c$::uidp uid)
                              (identp new-fn))))
  (declare (ignorable fundef uid new-fn))
  (fundef (c$::fundef->extension fundef)
          (decl-spec-list-rename-fn (c$::fundef->specs fundef)
                                    uid new-fn)
          (declor-rename-fn (fundef->declor fundef)
                            uid new-fn)
          (c$::fundef->asm? fundef)
          (attrib-spec-list-rename-fn (c$::fundef->attribs fundef)
                                      uid new-fn)
          (declon-list-rename-fn (c$::fundef->declons fundef)
                                 uid new-fn)
          (comp-stmt-rename-fn (c$::fundef->body fundef)
                               uid new-fn)
          (c$::fundef->info fundef)))

Theorem: fundefp-of-fundef-rename-fn

(defthm fundefp-of-fundef-rename-fn
  (b* ((fty::result (fundef-rename-fn fundef uid new-fn)))
    (fundefp fty::result))
  :rule-classes :rewrite)

Theorem: fundef-rename-fn-of-fundef-fix-fundef

(defthm fundef-rename-fn-of-fundef-fix-fundef
  (equal (fundef-rename-fn (fundef-fix fundef)
                           uid new-fn)
         (fundef-rename-fn fundef uid new-fn)))

Theorem: fundef-rename-fn-fundef-equiv-congruence-on-fundef

(defthm fundef-rename-fn-fundef-equiv-congruence-on-fundef
  (implies (c$::fundef-equiv fundef fundef-equiv)
           (equal (fundef-rename-fn fundef uid new-fn)
                  (fundef-rename-fn fundef-equiv uid new-fn)))
  :rule-classes :congruence)

Theorem: fundef-rename-fn-of-uid-fix-uid

(defthm fundef-rename-fn-of-uid-fix-uid
  (equal (fundef-rename-fn fundef (c$::uid-fix uid)
                           new-fn)
         (fundef-rename-fn fundef uid new-fn)))

Theorem: fundef-rename-fn-uid-equiv-congruence-on-uid

(defthm fundef-rename-fn-uid-equiv-congruence-on-uid
  (implies (c$::uid-equiv uid uid-equiv)
           (equal (fundef-rename-fn fundef uid new-fn)
                  (fundef-rename-fn fundef uid-equiv new-fn)))
  :rule-classes :congruence)

Theorem: fundef-rename-fn-of-ident-fix-new-fn

(defthm fundef-rename-fn-of-ident-fix-new-fn
  (equal (fundef-rename-fn fundef uid (ident-fix new-fn))
         (fundef-rename-fn fundef uid new-fn)))

Theorem: fundef-rename-fn-ident-equiv-congruence-on-new-fn

(defthm fundef-rename-fn-ident-equiv-congruence-on-new-fn
  (implies (c$::ident-equiv new-fn new-fn-equiv)
           (equal (fundef-rename-fn fundef uid new-fn)
                  (fundef-rename-fn fundef uid new-fn-equiv)))
  :rule-classes :congruence)