Defines sleep_heartbeats tactic.

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

def sleepAtLeastHeartbeats (n : Nat) : IO Unit

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.

Equations

• One or more equations did not get rendered due to their size.

def tacticSleep_heartbeats_ : Lean.ParserDescr

do nothing for at least n heartbeats

Equations

• One or more equations did not get rendered due to their size.