diff --git a/src/Std/Internal/Async/Basic.lean b/src/Std/Internal/Async/Basic.lean index 1b2774334969..387bdc8f22b0 100644 --- a/src/Std/Internal/Async/Basic.lean +++ b/src/Std/Internal/Async/Basic.lean @@ -90,7 +90,14 @@ def block (x : AsyncTask α) : IO α := do Create an `AsyncTask` that resolves to the value of `x`. -/ @[inline] -def ofPromise (x : IO.Promise α) : AsyncTask α := +def ofPromise (x : IO.Promise (Except IO.Error α)) : AsyncTask α := + x.result + +/-- +Create an `AsyncTask` that resolves to the value of `x`. +-/ +@[inline] +def ofPurePromise (x : IO.Promise α) : AsyncTask α := x.result.map pure /-- diff --git a/src/Std/Internal/Async/Timer.lean b/src/Std/Internal/Async/Timer.lean index fdaba3c0ec5b..e3fd6a77d66c 100644 --- a/src/Std/Internal/Async/Timer.lean +++ b/src/Std/Internal/Async/Timer.lean @@ -42,7 +42,7 @@ If: @[inline] def wait (s : Sleep) : IO (AsyncTask Unit) := do let promise ← s.native.next - return .ofPromise promise + return .ofPurePromise promise /-- If: @@ -108,7 +108,7 @@ If: @[inline] def tick (i : Interval) : IO (AsyncTask Unit) := do let promise ← i.native.next - return .ofPromise promise + return .ofPurePromise promise /-- If: