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 (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.

Equations

• IO.Promise α = IO.PromiseImpl✝ α

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

@[extern lean_io_promise_new]

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

Creates a new Promise.

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

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

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

@[deprecated IO.Promise.result! (since := "2025-02-05")]

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

• @IO.Promise.result = @IO.Promise.result!

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

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?