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 α) :

meta constant task.pure {α : Type u} (t : α) :
task α

meta constant {α : Type u} {β : Type v} (f : α → β) (t : task α) :
task β

meta constant task.flatten {α : Type u} :
task (task α)task α

meta def task.bind {α : Type u} {β : Type v} (t : task α) (f : α → task β) :
task β

meta def task.delay {α : Type u} (f : unit → α) :
task α