Documentation

Std.Internal.Async.Basic

@[inline]

Construct an AsyncTask that is already resolved with value x.

Equations
@[inline]
def Std.Internal.IO.Async.AsyncTask.bind {α : Type u_1} {β : Type u_2} (x : AsyncTask α) (f : αAsyncTask β) :

Create a new AsyncTask that will run after x has finished. If x:

  • errors, return an AsyncTask that resolves to the error.
  • succeeds, run f on the result of x and return the AsyncTask produced by f.
Equations
@[inline]
def Std.Internal.IO.Async.AsyncTask.map {α : Type u_1} {β : Type u_2} (f : αβ) (x : AsyncTask α) :

Create a new AsyncTask that will run after x has finished. If x:

  • errors, return an AsyncTask that reolves to the error.
  • succeeds, return an AsyncTask that resolves to f x.
Equations
@[inline]
def Std.Internal.IO.Async.AsyncTask.bindIO {α : Type u_1} {β : Type} (x : AsyncTask α) (f : αIO (AsyncTask β)) :

Similar to bind, however f has access to the IO monad. If f throws an error, the returned AsyncTask resolves to that error.

Equations
@[inline]
def Std.Internal.IO.Async.AsyncTask.mapIO {α : Type u_1} {β : Type} (f : αIO β) (x : AsyncTask α) :

Similar to bind, however f has access to the IO monad. If f throws an error, the returned AsyncTask resolves to that error.

Equations

Block until the AsyncTask in x finishes.

Equations
@[inline]

Create an AsyncTask that resolves to the value of x.

Equations