		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename-fn

Fundef-option-rename-fn

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

Definitions and Theorems

Function: fundef-option-rename-fn

(defun fundef-option-rename-fn (c$::fundef-option uid new-fn)
 (declare (xargs :guard (and (fundef-optionp c$::fundef-option)
                             (c$::uidp uid)
                             (identp new-fn))))
 (fundef-option-case
  c$::fundef-option
  :some
  (fundef-fix
   (fundef-rename-fn (c$::fundef-option-some->val c$::fundef-option)
                     uid new-fn))
  :none nil))

Theorem: fundef-optionp-of-fundef-option-rename-fn

(defthm fundef-optionp-of-fundef-option-rename-fn
  (b* ((fty::result
            (fundef-option-rename-fn c$::fundef-option uid new-fn)))
    (fundef-optionp fty::result))
  :rule-classes :rewrite)

Theorem: fundef-option-rename-fn-under-iff

(defthm fundef-option-rename-fn-under-iff
  (iff (fundef-option-rename-fn c$::fundef-option uid new-fn)
       c$::fundef-option))

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

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

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

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

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

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

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

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

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

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

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

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