mathlib documentation

core / init.meta.task

source
meta constant task  :
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
@[protected]
meta constant task.pure {α : Type u} (t : α) :
task α
source
@[protected]
meta constant task.map {α : Type u} {β : Type v} (f : α → β) (t : task α) :
task β
source
@[protected]
meta constant task.flatten {α : Type u} :
task (task α) → task α
source
@[protected]
meta def task.bind {α : Type u} {β : Type v} (t : task α) (f : α → task β) :
task β
source
meta def task.delay {α : Type u} (f : unit → α) :
task α