From 624e47abaa5846af0190c8dcd1828d061548e4a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 10 Jan 2025 17:01:16 +0100 Subject: [PATCH] chore: remove sorries --- tests/lean/run/async_surface_sleep.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/lean/run/async_surface_sleep.lean b/tests/lean/run/async_surface_sleep.lean index 23f6cf30b27e..b548fd058f2c 100644 --- 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