Lean4
/-- Guard the minimal number of heartbeats used in the enclosed command.
This is most useful in the context of debugging and minimizing an example of a slow declaration.
By guarding the number of heartbeats used in the slow declaration,
an error message will be generated if a minimization step makes the slow behaviour go away.
The default number of minimal heartbeats is the value of `maxHeartbeats` (typically 200000).
Alternatively, you can specify a number of heartbeats to guard against,
using the syntax `guard_min_heartbeats n in cmd`.
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 `guard_min_heartbeats approximately (n)? in cmd`.
-/
@[command_parser 1000]
public meta def commandGuard_min_heartbeatsApproximately_In__ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.CountHeartbeats.commandGuard_min_heartbeatsApproximately_In__ 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "guard_min_heartbeats ")
(ParserDescr.unary✝ `optional
((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "approximately " false✝)))
(ParserDescr.unary✝ `optional (ParserDescr.const✝ `num)))
(ParserDescr.symbol✝ "in"))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppLine)))
(ParserDescr.cat✝ `command 0))
