Searching commands

search $\lbrace$[ bound $\lbrace$,depth$\rbrace$ ]$\rbrace$ $\lbrace$in module :$\rbrace$ subject searchtype pattern $\lbrace$such that condition$\rbrace$ .

Performs a breadth-first search for rewrite proofs starting at subject to a final state that matches pattern and satisfies an optional condition (whose syntactic form is the same as the one of conditions for conditional equations and memberships; see Section 4.3). Possible values for searchtype are

=>1	one step proof
=>+	one or more steps proof
=>*	zero or more steps proof
=>!	only canonical final states, that cannot be further rewritten,
	are allowed as solutions

The optional bound argument provides an upper bound in the number of solutions to be found; if it is omitted, infinity is assumed.

The optional depth argument indicates the maximum depth of the search. If it is omitted, infinity is assumed. It is also possible to give a depth bound without giving a bound on the number of solutions returned by requesting a search of the form search [,m] ....

The search type =>1 is an abbreviation of the search type =>+ with the depth bound set to 1.

As usual, if the in clause is omitted, the current module is assumed.

For examples, see Section 5.4.3.

show search graph .

Displays the search graph generated by the last search.

show path number .

Displays the path to a given state, identified by the number, in a search graph.

show path labels number .

Works like the command above, but only shows labels of applied rules instead of the full path.