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. Use Promise.result? to handle this case 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. Use Promise.result? to handle this case 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