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.

Syntax

<set-reduction-strategy-command> ::= set reduction-strategy 
                                        ( inside-out | outside-in )

Note: The reduction-strategy can be abbreviated.

Examples

set reduction in

Usage

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 entire term.

The reduction-strategy is local to the current proof context.