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} :
task α → α

meta constant task.pure {α : Type u} :
α → task α

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

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

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

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