time : ('a -> 'b) -> 'a -> 'b

SYNOPSIS

Report CPU time taken by a function.

DESCRIPTION

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.

EXAMPLE

  # time NUM_REDUCE_CONV `123 EXP 14`;;
  CPU time (user): 0.09
  val it : thm = |- 123 EXP 14 = 181414317867238075368413196009

USES

Monitoring CPU time taken, e.g. to test different algorithms or implementation optimizations.

SEE ALSO

report_timing.