apply

apply <action> [ <subst> ] <range> <selection>

Applies one of the following actions reduce, exec, print, or a rewrite rule to the term in focus.

reduce, exec, print ~ the operation acts on the (sub)term specified by <range> and <selection>.

rewrite rule ~ in this case a rewrite rule spec has to be given in the following form:

`[+|-][<mod_name>].<rule-id>`

where `<mod_name>` is the name of a module, and `<rule-id>` either
a number n - in which case the n. equation in the current module
is used, or the label of an equation. If the `<mod_name>` is not
given, the equations of the current module are considered. If the
leading `+` or no leading character is given, the equation is
applied left-to-right, which with a leading `-` the equation is
applied right-to-left.

The <subst> is of the form

with { <var_name> = <term> } +,

and is used when applying a rewrite rule. In this case the variables in the rule are bound to the given term.

<range> is either within or at. In the former case the action is applied at or inside the (sub)term specified by the following selection. In the later case it means exactly at the (sub)term.

Finally, the <selection> is an expression

<selector> { of <selector> } *

where each <selector> is one of

top, term ~ Selects the whole term

subterm ~ Selects the pre-chosen subterm (see choose)

( <number_list> ) ~ A list of numbers separated by blanks as in (2 1) indicates a subterm by tree search. (2 1) means the first argument of the second argument.

[ <number1> .. <number2> ] ~ This selector can only be used with associative operators. It indicates a subterm in a flattened structure and selects the subterm between and including the two numbers given. [n .. n] can be abbreviated to [n].

Example: If the term is `a * b * c * d * e`, then the 
expression `[2 .. 4]` selects the subterm `b * c * d`.

{ <number_set> } ~ This selector can only be used with associative and commutative operators. It indicates a subterm in a multiset structure obtained from selecting the subterms at position given by the numbers.

Example: If the operator _*_ is declared as associative and commutative, and the current term is b * c * d * c * e, then then the expression {2, 4, 5} selects the subterm c * c * e.

Related: start, choose