time : ('a -> 'b) -> 'a -> 'b
Report CPU time taken by a function.
A call time f x will evaluate f x as usual, but will also (provided the
report_timing flag is true as it is by default) print the CPU time taken by
that function evaluation.
- FAILURE CONDITIONS
Never fails in itself, though it propagates any exception generated by the call
f x itself.
# time NUM_REDUCE_CONV `123 EXP 14`;;
CPU time (user): 0.09
val it : thm = |- 123 EXP 14 = 181414317867238075368413196009
Monitoring CPU time taken, e.g. to test different algorithms or implementation
- SEE ALSO