		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Ident-option-rename

Signature
(ident-option-rename ident-option subst) → fty::result
Arguments: ident-option — Guard (ident-optionp ident-option).; subst — Guard (ident-ident-alistp subst).
Returns: fty::result — Type (ident-optionp fty::result).

Definitions and Theorems

Function: ident-option-rename

(defun ident-option-rename (ident-option subst)
 (declare (xargs :guard (and (ident-optionp ident-option)
                             (ident-ident-alistp subst))))
 (let ((__function__ 'ident-option-rename))
   (declare (ignorable __function__))
   (c$::ident-option-case
        ident-option
        :some
        (ident-fix
             (ident-rename (c$::ident-option-some->val ident-option)
                           subst))
        :none nil)))

Theorem: ident-optionp-of-ident-option-rename

(defthm ident-optionp-of-ident-option-rename
  (b* ((fty::result (ident-option-rename ident-option subst)))
    (ident-optionp fty::result))
  :rule-classes :rewrite)

Theorem: ident-option-rename-under-iff

(defthm ident-option-rename-under-iff
  (iff (ident-option-rename ident-option subst)
       ident-option))

Theorem: ident-option-rename-of-ident-option-fix-ident-option

(defthm ident-option-rename-of-ident-option-fix-ident-option
  (equal (ident-option-rename (ident-option-fix ident-option)
                              subst)
         (ident-option-rename ident-option subst)))

Theorem: ident-option-rename-ident-option-equiv-congruence-on-ident-option

(defthm
  ident-option-rename-ident-option-equiv-congruence-on-ident-option
  (implies (c$::ident-option-equiv ident-option ident-option-equiv)
           (equal (ident-option-rename ident-option subst)
                  (ident-option-rename ident-option-equiv subst)))
  :rule-classes :congruence)

Theorem: ident-option-rename-of-ident-ident-alist-fix-subst

(defthm ident-option-rename-of-ident-ident-alist-fix-subst
  (equal (ident-option-rename ident-option
                              (ident-ident-alist-fix subst))
         (ident-option-rename ident-option subst)))

Theorem: ident-option-rename-ident-ident-alist-equiv-congruence-on-subst

(defthm
    ident-option-rename-ident-ident-alist-equiv-congruence-on-subst
  (implies (ident-ident-alist-equiv subst subst-equiv)
           (equal (ident-option-rename ident-option subst)
                  (ident-option-rename ident-option subst-equiv)))
  :rule-classes :congruence)