Lean4
/-- `#count_heartbeats! in cmd` runs a command `10` times, reporting the range in heartbeats, and the
standard deviation. The command `#count_heartbeats! n in cmd` runs it `n` times instead.
Example usage:
```
#count_heartbeats! in
def f := 37
```
displays the info message `Min: 7 Max: 8 StdDev: 14%`.
-/
@[command_parser 1000]
public meta def «command#count_heartbeats!_In__» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.CountHeartbeats.«command#count_heartbeats!_In__» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#count_heartbeats! ")
(ParserDescr.unary✝ `optional (ParserDescr.const✝ `num)))
(ParserDescr.symbol✝ "in"))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppLine)))
(ParserDescr.cat✝ `command 0))
