feat: add duration side condition for repeating timer

leanprover · Jan 7, 2025 · 52d5c1e · 52d5c1e
1 parent a5b05eb
commit 52d5c1e
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/Std/Internal/Async/Timer.lean b/src/Std/Internal/Async/Timer.lean
@@ -90,7 +90,7 @@ Setup up an `Interval` that waits for `duration` milliseconds.
 This function only initializes but does not yet start the timer.
 -/
 @[inline]
-def mk (duration : Std.Time.Millisecond.Offset) : IO Interval := do
+def mk (duration : Std.Time.Millisecond.Offset) (_ : 0 < duration := by decide) : IO Interval := do
   let native ← Internal.UV.Timer.mk duration.toInt.toNat.toUInt64 true
   return ofNative native
 

diff --git a/tests/lean/run/async_surface_sleep.lean b/tests/lean/run/async_surface_sleep.lean
@@ -63,7 +63,7 @@ def oneSleep : IO Unit := do
   assert! (← task.block) == 37
 where
   go : IO (AsyncTask Nat) := do
-    let interval ← Interval.mk BASE_DURATION
+    let interval ← Interval.mk BASE_DURATION sorry
     (← interval.tick).mapIO fun _ => do
       interval.stop
       return 37
@@ -73,7 +73,7 @@ def doubleSleep : IO Unit := do
   assert! (← task.block) == 37
 where
   go : IO (AsyncTask Nat) := do
-    let interval ← Interval.mk BASE_DURATION
+    let interval ← Interval.mk BASE_DURATION sorry
     (← interval.tick).bindIO fun _ => do
     (← interval.tick).mapIO fun _ => do
       interval.stop
@@ -84,7 +84,7 @@ def resetSleep : IO Unit := do
   assert! (← task.block) == 37
 where
   go : IO (AsyncTask Nat) := do
-    let interval ← Interval.mk BASE_DURATION
+    let interval ← Interval.mk BASE_DURATION sorry
     (← interval.tick).bindIO fun _ => do
       let waiter ← interval.tick
       interval.reset