Documentation

Batteries.Lean.System.IO

Functions for manipulating a list of tasks #

def IO.waitAny' {α : Type} (tasks : List (Task α)) (h : autoParam (0 < tasks.length) _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.
Instances For
    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
    Instances For