		Search-engine friendly clone of the ACL2 documentation.

Renaming

Alternation-rename-rule

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

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

Function: alternation-rename-rule

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