monitoring
computeLib.monitoring : (term -> bool) option ref
Monitoring support for evaluation.
The reference variable monitoring provides a simple way to view the
operation of EVAL, EVAL_RULE, and EVAL_TAC. The initial value of
monitoring is NONE. If one wants to monitor the expansion of a
function, defined with constant c, then setting monitoring to
SOME (same_const c) will tell the system to print out the expansion of
c by the evaluation entrypoints. To monitor the expansions of a
collection of functions, defined with c1,...,cn, then monitoring
can be set to
SOME (fn x => same_const c1 x orelse ... orelse same_const cn x)
Failure
Never fails.
Example
> val [FACT] = decls "FACT";
val FACT = “FACT”: term
> computeLib.monitoring := SOME (same_const FACT);
val it = (): unit
> EVAL (Term `FACT 4`);
FACT 4 = 4 * FACT 3
FACT 3 = 3 * FACT (PRE 3)
FACT 2 = 2 * FACT 1
FACT 1 = 1 * FACT (PRE 1)
FACT 0 = 1
val it = ⊢ FACT 4 = 24: thm