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