chore: 0th interval

leanprover · Jan 2, 2025 · 4199e25 · 4199e25
1 parent a85bdd4
commit 4199e25
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/tests/lean/run/async_sleep.lean b/tests/lean/run/async_sleep.lean
@@ -212,6 +212,8 @@ def sequentialSleep : IO Unit := do
 where
   go : IO (AsyncTask Unit) := do
     let t ← Interval.mk 10
+    -- 0th interval ticks instantly
+    (← t.tick).bindIO fun _ => do
     (← t.tick).bindIO fun _ => do
     (← t.tick).mapIO fun _ => ()