		Search-engine friendly clone of the ACL2 documentation.

Renaming

Rule-rename-rule

Rename all the occurrences of a rule name to a new rule name, both in the definiens of a rule and in the name of the rule itself.

Signature
(rule-rename-rule rule oldname newname) → new-rule
Arguments: rule — Guard (rulep rule).; oldname — Guard (rulenamep oldname).; newname — Guard (rulenamep newname).
Returns: new-rule — Type (rulep new-rule).

Definitions and Theorems

Function: rule-rename-rule

(defun rule-rename-rule (rule oldname newname)
  (declare (xargs :guard (and (rulep rule)
                              (rulenamep oldname)
                              (rulenamep newname))))
  (make-rule
       :name
       (if (equal (rule->name rule) oldname)
           newname
         (rule->name rule))
       :incremental (rule->incremental rule)
       :definiens (alternation-rename-rule (rule->definiens rule)
                                           oldname newname)))

Theorem: rulep-of-rule-rename-rule

(defthm rulep-of-rule-rename-rule
  (b* ((new-rule (rule-rename-rule rule oldname newname)))
    (rulep new-rule))
  :rule-classes :rewrite)