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
    @[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.