Functions for manipulating a list of tasks

• IO.waitAny' is a wrapper for IO.waitAny that also returns the remaining tasks.
• List.waitAll : List (Task α) → Task (List α) gathers a list of tasks into a task returning the list of all results.

def IO.waitAny' {α : Type} (tasks : List (Task α)) (h : autoParam (0 < List.length tasks) _auto✝) : BaseIO (α × List (Task α))

Given a non-empty list of tasks, wait for the first to complete. Return the value and the list of remaining tasks.

Equations

• One or more equations did not get rendered due to their size.

def List.waitAll {α : Type u_1} (tasks : List (Task α)) : Task (List α)

Given a list of tasks, create the task returning the list of results, by waiting for each.

Equations

• List.waitAll [] = { get := [] }
• List.waitAll (task :: tasks_2) = Task.bind task (fun (a : α) => Task.map (fun (as : List α) => a :: as) (List.waitAll tasks_2) Task.Priority.max) Task.Priority.max