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.

@[extern lean_io_promise_new]
opaque {α : Type} [inst : 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.