@[noinline]

def IO.waitAny {α : Type} (tasks : List (Task α)) (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) : BaseIO α

Waits until any of the tasks in the list has finished, then return its result.

Equations

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

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 []