mathlib documentation

core.init.meta.task

source
meta constant task (a : Type u) :
Type u

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

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

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

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

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

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

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