def IO.Promise (α : Type) : 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

• IO.Promise α = IO.PromiseImpl✝ α

theorem IO.instNonemptyPromise {α : Type} [s : Nonempty α] : Nonempty (IO.Promise α)

@[extern lean_io_promise_new]

opaque IO.Promise.new {α : Type} [Nonempty α] : BaseIO (IO.Promise α)

Creates a new Promise.

@[extern lean_io_promise_resolve]

opaque IO.Promise.resolve {α : Type} (value : α) (promise : IO.Promise α) : BaseIO Unit

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.