Lean 4 (Meta)programming Cookbook

Putting a Process to Sleep🔗

You can pause the current thread using IO.sleep. It takes the duration in milliseconds.

def delayedHello : IO Unit := do IO.println "Wait for it..." IO.sleep 2000 -- Wait for 2 seconds IO.println "Hello Lean!"

Note that IO.sleep is non-blocking for other Lean tasks; it only pauses the current execution flow.