		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-rename

Declon-list-rename

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

Definitions and Theorems

Theorem: declon-list-rename-type-prescription

(defthm declon-list-rename-type-prescription
  (true-listp (declon-list-rename c$::declon-list subst))
  :rule-classes :type-prescription)

Theorem: declon-list-rename-when-atom

(defthm declon-list-rename-when-atom
  (implies (atom c$::declon-list)
           (equal (declon-list-rename c$::declon-list subst)
                  nil)))

Theorem: declon-list-rename-of-cons

(defthm declon-list-rename-of-cons
  (equal (declon-list-rename (cons declon c$::declon-list)
                             subst)
         (cons (declon-rename declon subst)
               (declon-list-rename c$::declon-list subst))))

Theorem: declon-list-rename-of-append

(defthm declon-list-rename-of-append
  (equal (declon-list-rename (append acl2::x acl2::y)
                             subst)
         (append (declon-list-rename acl2::x subst)
                 (declon-list-rename acl2::y subst))))

Theorem: consp-of-declon-list-rename

(defthm consp-of-declon-list-rename
  (equal (consp (declon-list-rename c$::declon-list subst))
         (consp c$::declon-list)))

Theorem: len-of-declon-list-rename

(defthm len-of-declon-list-rename
  (equal (len (declon-list-rename c$::declon-list subst))
         (len c$::declon-list)))

Theorem: nth-of-declon-list-rename

(defthm nth-of-declon-list-rename
  (equal (nth acl2::n
              (declon-list-rename c$::declon-list subst))
         (if (< (nfix acl2::n) (len c$::declon-list))
             (declon-rename (nth acl2::n c$::declon-list)
                            subst)
           nil)))

Theorem: declon-list-rename-of-revappend

(defthm declon-list-rename-of-revappend
  (equal (declon-list-rename (revappend acl2::x acl2::y)
                             subst)
         (revappend (declon-list-rename acl2::x subst)
                    (declon-list-rename acl2::y subst))))

Theorem: declon-list-rename-of-reverse

(defthm declon-list-rename-of-reverse
  (equal (declon-list-rename (reverse c$::declon-list)
                             subst)
         (reverse (declon-list-rename c$::declon-list subst))))