Defines #time
command. #
Time the elaboration of a command, and print the result (in milliseconds).
Equations
- timeCmd = Lean.ParserDescr.node `timeCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#time ") (Lean.ParserDescr.cat `command 0))
Instances For
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.