		Search-engine friendly clone of the ACL2 documentation.

Renaming

Element-rename-rule

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

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

Function: element-rename-rule

(defun element-rename-rule (element oldname newname)
 (declare (xargs :guard (and (elementp element)
                             (rulenamep oldname)
                             (rulenamep newname))))
 (element-case
  element :rulename
  (if (equal element.get oldname)
      (element-rulename newname)
    (element-fix element))
  :group (element-group
              (alternation-rename-rule element.get oldname newname))
  :option
  (element-option
       (alternation-rename-rule element.get oldname newname))
  :char-val (element-fix element)
  :num-val (element-fix element)
  :prose-val (element-fix element)))