		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Const-rename

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

Definitions and Theorems

Function: const-rename

(defun const-rename (c$::const subst)
 (declare (xargs :guard (and (constp c$::const)
                             (ident-ident-alistp subst))))
 (declare (ignorable c$::const subst))
 (let ((__function__ 'const-rename))
  (declare (ignorable __function__))
  (const-case
    c$::const
    :int (c$::const-int (iconst-rename (const-int->unwrap c$::const)
                                       subst))
    :float (const-fix c$::const)
    :enum
    (c$::const-enum (ident-rename (c$::const-enum->unwrap c$::const)
                                  subst))
    :char (const-fix c$::const))))

Theorem: constp-of-const-rename

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

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

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

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

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

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

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

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

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