The Lean Language Reference

21.8. Timing🔗

🔗opaque

Pauses execution for the specified number of milliseconds.

🔗opaque

Monotonically increasing time since an unspecified past point in nanoseconds. There is no relation to wall clock time.

🔗opaque

Monotonically increasing time since an unspecified past point in milliseconds. There is no relation to wall clock time.

🔗opaque

Returns the number of heartbeats that have occurred during the current thread's execution. The heartbeat count is the number of "small" memory allocations performed in a thread.

Heartbeats used to implement timeouts that are more deterministic across different hardware.

🔗def

Adjusts the heartbeat counter of the current thread by the given amount. This can be useful to give allocation-avoiding code additional “weight” and is also used to adjust the counter after resuming from a snapshot.

Heartbeats are a means of implementing “deterministic” timeouts. The heartbeat counter is the number of “small” memory allocations performed on the current execution thread.