Documentation

Mathlib.Util.Time

Defines #time command. #

Time the elaboration of a command, and print the result (in milliseconds).

Time the elaboration of a command, and print the result (in milliseconds).

Example usage:

set_option maxRecDepth 100000 in
#time example : (List.range 500).length = 500 := rfl
Equations
  • One or more equations did not get rendered due to their size.
Instances For