		Search-engine friendly clone of the ACL2 documentation.

Renaming

Rulelist-rename-rule

Rename all the occurrences of a rule name to a new rule name, in all the rules in a list of rules.

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

Definitions and Theorems

Function: rulelist-rename-rule

(defun rulelist-rename-rule (rules oldname newname)
  (declare (xargs :guard (and (rulelistp rules)
                              (rulenamep oldname)
                              (rulenamep newname))))
  (cond ((endp rules) nil)
        (t (cons (rule-rename-rule (car rules)
                                   oldname newname)
                 (rulelist-rename-rule (cdr rules)
                                       oldname newname)))))

Theorem: rulelistp-of-rulelist-rename-rule

(defthm rulelistp-of-rulelist-rename-rule
  (b* ((new-rules (rulelist-rename-rule rules oldname newname)))
    (rulelistp new-rules))
  :rule-classes :rewrite)