		Search-engine friendly clone of the ACL2 documentation.

Rename

Rename-const

Signature
(rename-const const subst) → new-const
Arguments: const — Guard (constp const).; subst — Guard (ident-ident-alistp subst).
Returns: new-const — Type (constp new-const).

Definitions and Theorems

Function: rename-const

(defun rename-const (const subst)
  (declare (xargs :guard (and (constp const)
                              (ident-ident-alistp subst))))
  (declare (ignorable const subst))
  (let ((__function__ 'rename-const))
    (declare (ignorable __function__))
    (const-fix const)))

Theorem: constp-of-rename-const

(defthm constp-of-rename-const
  (b* ((new-const (rename-const const subst)))
    (constp new-const))
  :rule-classes :rewrite)