Defines a command wrapper that prints the number of heartbeats used in the enclosed command.
count_heartbeats in theorem foo : 42 = 6 * 7 := rfl
will produce an info message containing a number around 51.
If this number is above the current
maxHeartbeats, we also print a
Try this: suggestion.
Count the heartbeats used in the enclosed command.
This is most useful for setting sufficient but reasonable limits via
for long running declarations.
If you do so, please resist the temptation to set the limit as low as possible.
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_heartbearts 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 that internal heartbeat counter accessible via
has granularity 1000 times finer that the limits set by
As this is intended as a user command, we divide by 1000.