def IO.Promise (α : Type) :

Promise α allows you to create a Task α whose value is provided later by calling resolve.

Typical usage is as follows:

  1. let promise ← creates a promise
  2. promise.result : Task α can now be passed around
  3. promise.result.get blocks until the promise is resolved
  4. promise.resolve a resolves the promise
  5. promise.result.get now returns a

Every promise must eventually be resolved. Otherwise the memory used for the promise will be leaked, and any tasks depending on the promise's result will wait forever.

Instances For
    instance IO.instNonemptyPromise {α : Type} [s : Nonempty α] :
    • =
    @[extern lean_io_promise_new]
    opaque {α : Type} [Nonempty α] :

    Creates a new Promise.

    @[extern lean_io_promise_resolve]
    opaque IO.Promise.resolve {α : Type} (value : α) (promise : IO.Promise α) :

    Resolves a Promise.

    Only the first call to this function has an effect.

    @[extern lean_io_promise_result]
    opaque IO.Promise.result {α : Type} (promise : IO.Promise α) :
    Task α

    The result task of a Promise.

    The task blocks until Promise.resolve is called.