REN-VAR-FN : FLAGREN-VAR-FN is a flag or parameter.
The value of this flag is a function to be called when a variable
must be renamed automatically. It has three possible settings:
REN-VAR-X1 is the standard renaming function. It renames y to y^1,
then to y^2, and so on. If there is another variable y, of a different
type, it makes no difference.
REN-VAR-X11 is much like REN-VAR-X1, except it will avoid creating
two variables of the same name at different types (so it tends to
produce higher exponents than REN-VAR-X1).
REN-VAR-XA renames alphabetically, turning y into ya, then yba,
and so on.
REN-VAR-FN takes values of type SYMBOL.
It belongs to subjects WFF-PRIMS .
Its default value is REN-VAR-X1
Its current value is REN-VAR-X1.
ETPS documentation homepage