Defines #time command.

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

ink

def timeCmd : Lean.ParserDescr

Equations

• timeCmd = Lean.ParserDescr.node `timeCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#time ") (Lean.ParserDescr.cat `command 0))

ink

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

Equations

• One or more equations did not get rendered due to their size.