chore: remove sorries

leanprover · Jan 10, 2025 · 624e47a · 624e47a
1 parent b6c2038
commit 624e47a
Showing 1 changed file with 3 additions and 3 deletions.
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 sorry
+    let interval ← Interval.mk BASE_DURATION
     (← 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 sorry
+    let interval ← Interval.mk BASE_DURATION
     (← 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 sorry
+    let interval ← Interval.mk BASE_DURATION
     (← interval.tick).bindIO fun _ => do
       let waiter ← interval.tick
       interval.reset