Documentation

Batteries.Lean.System.IO

Functions for manipulating a list of tasks #

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
  • [].waitAll = { get := [] }
  • (task :: tasks_2).waitAll = task.bind (fun (a : α) => Task.map (fun (as : List α) => a :: as) tasks_2.waitAll Task.Priority.max) Task.Priority.max
Instances For