Defines sleep_heartbeats tactic. #

This is useful for testing / debugging long running commands or elaboration in a somewhat precise manner.

A low level command to sleep for at least a given number of heartbeats by running in a loop until the desired number of heartbeats is hit. Warning: this function relies on interpreter / compiler behaviour that is not guaranteed to function in the way that is relied upon here. As such this function is not to be considered reliable, especially after future updates to Lean. This should be used with caution and basically only for demo / testing purposes and not in compiled code without further testing.

Instances For

    do nothing for at least n heartbeats

    Instances For