Lean4
/-- `#count_heartbeats in cmd` counts the heartbeats used in the enclosed command `cmd`.
Use `#count_heartbeats` to count the heartbeats in *all* the following declarations.
This is most useful for setting sufficient but reasonable limits via `set_option maxHeartbeats`
for long-running declarations.
If you do so, please resist the temptation to set the limit as low as possible.
As the `simp` set and other features of the library evolve,
other contributors will find that their (likely unrelated) changes
have pushed the declaration over the limit.
`count_heartbeats in` will automatically suggest a `set_option maxHeartbeats` via "Try this:"
using the least number of the form `2^k * 200000` that suffices.
Note that the internal heartbeat counter accessible via `IO.getNumHeartbeats`
has granularity 1000 times finer than the limits set by `set_option maxHeartbeats`.
As this is intended as a user command, we divide by 1000.
The optional `approximately` keyword rounds down the heartbeats to the nearest thousand.
This helps make the tests more stable to small changes in heartbeats.
To use this functionality, use `#count_heartbeats approximately in cmd`.
-/
@[command_parser 1000]
public meta def «command#count_heartbeatsApproximatelyIn__» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.CountHeartbeats.«command#count_heartbeatsApproximatelyIn__» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#count_heartbeats ")
(ParserDescr.unary✝ `optional
((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "approximately " false✝)))
(ParserDescr.symbol✝ "in"))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppLine)))
(ParserDescr.cat✝ `command 0))
