chore: intermediate

leanprover · Jan 5, 2025 · 2272faa · 2272faa
1 parent 7109127
commit 2272faa
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 3 deletions.
diff --git 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
@@ -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: