inductive IO.AsyncList (ε : Type u) (α : Type v) :
Type (maxuv)

An async IO list is like a lazy list but instead of being unevaluated Thunks, delayed suffixes are Tasks being evaluated asynchronously. A delayed suffix can signal the end of computation (successful or due to a failure) with a terminating value of type ε.

Instances For
    instance IO.AsyncList.instInhabitedAsyncList {ε : Type u_1} {α : Type u_2} :
    • IO.AsyncList.instInhabitedAsyncList = { default := IO.AsyncList.nil }
    partial def IO.AsyncList.append {ε : Type u_1} {α : Type u_2} :
    IO.AsyncList ε αIO.AsyncList ε αIO.AsyncList ε α
    instance IO.AsyncList.instAppendAsyncList {ε : Type u_1} {α : Type u_2} :
    • IO.AsyncList.instAppendAsyncList = { append := IO.AsyncList.append }
    def IO.AsyncList.ofList {α : Type u_1} {ε : Type u_2} :
    List αIO.AsyncList ε α
    • IO.AsyncList.ofList = List.foldr IO.AsyncList.cons IO.AsyncList.nil
    instance IO.AsyncList.instCoeListAsyncList {α : Type u_1} {ε : Type u_2} :
    Coe (List α) (IO.AsyncList ε α)
    • IO.AsyncList.instCoeListAsyncList = { coe := IO.AsyncList.ofList }
    def IO.AsyncList.unfoldAsync {σ : Type} {ε : Type} {α : Type} (f : StateT σ (EIO ε) (Option α)) (init : σ) :

    A stateful step computation f is applied iteratively, forming an async stream. The stream ends once f returns none for the first time.

    For cooperatively cancelling an ongoing computation, we recommend referencing a cancellation token in f and checking it when appropriate.

    partial def IO.AsyncList.unfoldAsync.step {σ : Type} {ε : Type} {α : Type} (f : StateT σ (EIO ε) (Option α)) (s : σ) :
    EIO ε (IO.AsyncList ε α)
    partial def IO.AsyncList.getAll {ε : Type u_1} {α : Type u_2} :
    IO.AsyncList ε αList α × Option ε

    The computed, synchronous list. If an async tail was present, returns also its terminating value.

    partial def IO.AsyncList.waitAll {α : Type u_1} {ε : Type u_2} (p : optParam (αBool) fun x => true) :
    IO.AsyncList ε αTask (List α × Option ε)

    Spawns a Task waiting on the prefix of elements for which p is true.

    partial def IO.AsyncList.waitFind? {α : Type u_1} {ε : Type u_2} (p : αBool) :
    IO.AsyncList ε αTask (Except ε (Option α))

    Spawns a Task acting like List.find? but which will wait for tail evalution when necessary to traverse the list. If the tail terminates before a matching element is found, the task throws the terminating value.

    partial def IO.AsyncList.getFinishedPrefix {ε : Type} {α : Type} :
    IO.AsyncList ε αBaseIO (List α × Option ε)

    Retrieve the already-computed prefix of the list. If computation has finished with an error, return it as well.

    def IO.AsyncList.waitHead? {ε : Type u_1} {α : Type u_2} (as : IO.AsyncList ε α) :
    Task (Except ε (Option α))