source
structure 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 (Option α)` 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 `some a`

If the promise is dropped without ever being resolved, `promise.result?.get` will return `none`. See `Promise.result!/resultD` for other ways to handle this case.

- prom : IO.PromisePointed✝.type
- h : Nonempty α

Instances For

source
instance IO.instNonemptyPromise {α : Type} [s : Nonempty α] :
Nonempty (Promise α)
source
@[extern lean_io_promise_new]
opaque IO.Promise.new {α : Type} [Nonempty α] :
BaseIO (Promise α)

Creates a new `Promise`.

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

Resolves a `Promise`.

Only the first call to this function has an effect.

source
@[extern lean_io_promise_result_opt]
opaque IO.Promise.result? {α : Type} (promise : Promise α) :
Task (Option α)

Like `Promise.result`, but resolves to `none` if the promise is dropped without ever being resolved.

source
def IO.Promise.result! {α : Type} (promise : Promise α) :
Task α

The result task of a `Promise`.

The task blocks until `Promise.resolve` is called. If the promise is dropped without ever being resolved, evaluating the task will panic and, when not using fatal panics, block forever. As `Promise.result!` is a pure value and thus the point of evaluation may not be known precisely, this means that any promise on which `Promise.result!` may be evaluated must be resolved eventually. When in doubt, always prefer `Promise.result?` to handle dropped promises explicitly.

Equations

- promise.result! = Task.map IO.Option.getOrBlock!✝ promise.result? Task.Priority.default true

Instances For

source
@[macro_inline]
def IO.Promise.resultD {α : Type} (promise : Promise α) (dflt : α) :
Task α

Like `Promise.result`, but resolves to `dflt` if the promise is dropped without ever being resolved.

Equations

- promise.resultD dflt = Task.map (fun (x : Option α) => x.getD dflt) promise.result? Task.Priority.default true

Instances For

source
def IO.Promise.isResolved {α : Type} (promise : Promise α) :
BaseIO Bool

Checks whether the promise has already been resolved, i.e. whether access to `result*` will return immediately.

Equations

- promise.isResolved = IO.hasFinished promise.result?

Instances For