Debugger commands

set break on . / set break off .

Controls whether break points are obeyed.

break select symbols . / break deselect symbols .

Selects/deselects operator symbols and labels from the current module for break points with the select option. Examples:

  break select foo bar baz .
  break deselect baz .

debug reduce $\lbrace$in module :$\rbrace$ term .

Works just like the reduce command in Section 16.2, except that it drops into the debugger before executing the first rewrite.

debug rewrite $\lbrace$[ number ]$\rbrace$ $\lbrace$in module :$\rbrace$ term .

Works just like the rewrite command in Section 16.2, except that it drops into the debugger before executing the first rewrite.

debug frewrite $\lbrace$[ bound $\lbrace$,number$\rbrace$ ]$\rbrace$ $\lbrace$in module :$\rbrace$ term .

Works just like the frewrite command in Section 16.2, except that it drops into the debugger before executing the first rewrite.

debug erewrite $\lbrace$[ bound $\lbrace$,number$\rbrace$ ]$\rbrace$ $\lbrace$in module :$\rbrace$ term .

Works just like the erewrite command in Section 16.2, except that it drops into the debugger before executing the first rewrite.

resume .

Only usable from the debugger. Exits the debugger and resumes the current rewriting activity.

abort .

Only usable from the debugger. Exits the debugger and abandons the current rewriting activity.

step .

Only usable from the debugger. Performs a single step of the current rewriting activity with tracing switched on.

where .

Only usable from the debugger. Prints the stack of pending rewrite tasks together with explanations of how they arose.