		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Const-option-rename

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

Definitions and Theorems

Function: const-option-rename

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

Theorem: const-optionp-of-const-option-rename

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

Theorem: const-option-rename-under-iff

(defthm const-option-rename-under-iff
  (iff (const-option-rename c$::const-option subst)
       c$::const-option))

Theorem: const-option-rename-of-const-option-fix-const-option

(defthm const-option-rename-of-const-option-fix-const-option
 (equal (const-option-rename (c$::const-option-fix c$::const-option)
                             subst)
        (const-option-rename c$::const-option subst)))

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

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

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

(defthm const-option-rename-of-ident-ident-alist-fix-subst
  (equal (const-option-rename c$::const-option
                              (ident-ident-alist-fix subst))
         (const-option-rename c$::const-option subst)))

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

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