Defines #time command.

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

def timeCmd : Lean.ParserDescr

def timeCmdElab : Lean.Elab.Command.CommandElab

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