		Search-engine friendly clone of the ACL2 documentation.

Renaming

Concatenation-rename-rule

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

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

Function: concatenation-rename-rule

(defun concatenation-rename-rule (concatenation oldname newname)
  (declare (xargs :guard (and (concatenationp concatenation)
                              (rulenamep oldname)
                              (rulenamep newname))))
  (cond ((endp concatenation) nil)
        (t (cons (repetition-rename-rule (car concatenation)
                                         oldname newname)
                 (concatenation-rename-rule (cdr concatenation)
                                            oldname newname)))))