		Search-engine friendly clone of the ACL2 documentation.

Copy-fn

Rename-fn-const

Signature
(rename-fn-const const old-fn new-fn) → new-const
Arguments: const — Guard (constp const).; old-fn — Guard (identp old-fn).; new-fn — Guard (identp new-fn).
Returns: new-const — Type (constp new-const).

Definitions and Theorems

Function: rename-fn-const

(defun rename-fn-const (const old-fn new-fn)
  (declare (xargs :guard (and (constp const)
                              (identp old-fn)
                              (identp new-fn))))
  (declare (ignorable const old-fn new-fn))
  (let ((__function__ 'rename-fn-const))
    (declare (ignorable __function__))
    (const-fix const)))

Theorem: constp-of-rename-fn-const

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