Tracing produces detailed information about each rewrite performed and
each conditional rewrite attempted. Since this typically results in an
unmanageably huge volume of output there are commands to control
what is actually displayed.
set trace on . / set trace off .
These commands turn tracing on and off.
If tracing is turned on, all trace information will be generated
internally even if none of it is displayed, thus considerably slowing
the speed of interpretation.
set trace condition on . / set trace condition off .
Determines whether the evaluations of conditions are traced.
set trace whole on . / set trace whole off .
Determines whether the whole term is printed before and after a rewrite.
set trace substitution on . / set trace substitution
off .
Determines whether the substitution is printed.
set trace mb on . / set trace mb off .
Determines whether membership axiom applications are printed.
set trace eq on . / set trace eq off .
Determines whether equation applications are printed.
set trace rl on . / set trace rl off .
Determines whether rule applications are printed.
set trace select on . / set trace select off .
Determines whether only trace information for selected operator
symbols is printed (rather than all symbols).
trace select symbols . / trace deselect symbols .
Selects/deselects operator symbols from the current module for tracing
with the select option. Examples:
