match

match <term_spec> to <pattern> .

Matches the term denoted by <term_spec> to the pattern. <term_spec> is either top or term for the term set by the start command; subterm for the term selected by the choose command; it has the same meaning as subterm if choose was used, otherwise the same meaning as top, or a normal term expression.

The given <pattern> is either rules, -rules, +rules, one of these three prefixed by all, or a term. If one of the rules are given, all the rules where the left side (for +rules), the right side (for -rules), or any side (for rules) matches. If the all (with separating space) is given all rules in the current context, including those declared in built-in modules, are inspected.

If a term is given, then the two terms are matched, and if successful, the matching substitution is printed.