		Search-engine friendly clone of the ACL2 documentation.

Renaming

Repetition-rename-rule

Rename all the occurrences of a rule name in a repetition to a new rule name.

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

Function: repetition-rename-rule

(defun repetition-rename-rule (repetition oldname newname)
 (declare (xargs :guard (and (repetitionp repetition)
                             (rulenamep oldname)
                             (rulenamep newname))))
 (make-repetition
      :range (repetition->range repetition)
      :element (element-rename-rule (repetition->element repetition)
                                    oldname newname)))