LP, the Larch Prover -- The reduction-strategy setting
The reduction-strategy setting controls the order in which LP applies
rewrite rules when reducing a term.
Note: The reduction-strategy can be
<set-reduction-strategy-command> ::= set reduction-strategy
( inside-out | outside-in )
set reduction in
When the reduction-strategy is outside-in (the default), LP attempts
to reduce a term by attempting to rewrite the entire term
before attempting to reduce any of its subterms. If it is inside-out, LP
still applies the hardwired rewrite rules outside-in, but it attempts to apply
other rewrite rules to the subterms of a term before it applies them to the
The reduction-strategy is local to the current proof context.