APPLY-RRULE-1* : WFFOP

APPLY-RRULE-1* is a wff operation.
Apply a rewrite rule (active or inactive) repeatedly
to the current edwff. If the rule is bidirectional, you will
be prompted about which direction to apply it in.
CAUTION: may not terminate.
 
The calling scheme for APPLY-RRULE-1* is:

(APPLY-RRULE-1* GWFF RULE)
"GWFF" "SYMBOL"


The result is of type GWFF.

The arguments have the following meaning:
GWFF : gwff before rewriting
RULE : name of rule

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage