def Task.mapList {α : Type u_1} {β : Type u_2} (f : List α → β) (tasks : List (Task α)) (prio : Priority := Priority.default) (sync : Bool := false) : Task β

Creates a task that, when all tasks have finished, computes the result of f applied to their results.

Equations

• Task.mapList f tasks prio sync = Task.mapList.go f prio sync tasks []

def Task.mapList.go {α : Type u_1} {β : Type u_2} (f : List α → β) (prio : Priority := Priority.default) (sync : Bool := false) : List (Task α) → List α → Task β

Equations

• Task.mapList.go f prio sync [] x✝ = if sync = true then { get := f x✝.reverse } else Task.spawn (fun (x : Unit) => f x✝.reverse) prio
• Task.mapList.go f prio sync [t] x✝ = Task.map (fun (a : α) => f (a :: x✝).reverse) t prio sync
• Task.mapList.go f prio sync (t :: ts) x✝ = t.bind (fun (a : α) => Task.mapList.go f prio sync ts (a :: x✝)) prio sync