mathlib documentation

core / init.meta.task

meta constant task  :
Type uType u

A task is a promise to produce a value later. They perform the same role as promises in JavaScript.

meta constant task.get {α : Type u} (t : task α) :
α
@[protected]
meta constant task.pure {α : Type u} (t : α) :
task α
@[protected]
meta constant task.map {α : Type u} {β : Type v} (f : α → β) (t : task α) :
task β
@[protected]
meta constant task.flatten {α : Type u} :
task (task α)task α
@[protected]
meta def task.bind {α : Type u} {β : Type v} (t : task α) (f : α → task β) :
task β
meta def task.delay {α : Type u} (f : unit → α) :
task α