Documentation

Init.System.Promise

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 ← Promise.new 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.

Equations
Instances For
    Equations
    @[extern lean_io_promise_new]
    opaque IO.Promise.new {α : 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.

    @[implemented_by _private.Init.System.Promise.0.IO.Promise.resultImpl]
    opaque IO.Promise.result {α : Type} (promise : IO.Promise α) :
    Task α

    The result task of a Promise.

    The task blocks until Promise.resolve is called.