Concise Rewriting Tactics

Unfolds as c

Unfold all visible occurrences of abstractions listed in the token list as in clause c

Unfold a c Unfolds [a] c

Repeatedly try unfolding any occurrences of abstractions listed in the token list as in clause c

Folds as c

Fold all visible occurrences of abstractions listed in the token list as in clause c

Fold a c Folds [a] c

Reduce c

Repeatedly contract all both primitive and abstract redices in clause c.

The Reduce tactic can take an optional force argument . The tactic

only reduces those redices with strength less than or equal to force. For more on defining abstract redices and setting the strength of redices, see Section and Section .

A couple of rewrite tactics provide access to all kinds of rewrite rules. These tactics take a control string  to specify the rewrite rules to use. Control string should be a whitespace-seperated list of tokens as specified in Table .

  
Table: Format of Tokens in Rewrite Control Strings

The tactics are:

RWW ( ctl-str : string) i

Repeatedly apply rewrite rules specified by ctl-str to all nodes of clause i until no further progress is made.

Apply rewrite rules specified by ctl-str in one top-down pass over clause i. If one of the rewrite rules succeeds on some subterm, then don't try rewriting the subterms of the rewritten subterm.