Documentation

Lean.Server.AsyncList

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

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} :
    Equations
    • 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} :
    Equations
    • IO.AsyncList.instAppendAsyncList = { append := IO.AsyncList.append }
    def IO.AsyncList.ofList {α : Type u_1} {ε : Type u_2} :
    List αIO.AsyncList ε α
    Equations
    • IO.AsyncList.ofList = List.foldr IO.AsyncList.cons IO.AsyncList.nil
    Instances For
      instance IO.AsyncList.instCoeListAsyncList {α : Type u_1} {ε : Type u_2} :
      Coe (List α) (IO.AsyncList ε α)
      Equations
      • 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.

      Equations
      Instances For
        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.waitUntil {α : Type u_1} {ε : Type u_2} (p : αBool) :
        IO.AsyncList ε αTask (List α × Option ε)

        Spawns a Task returning the prefix of elements up to (including) the first element for which p is true. When p is not true of any element, it returns the entire list.

        def IO.AsyncList.waitAll {ε : Type u_1} {α : Type u_2} :
        IO.AsyncList ε αTask (List α × Option ε)

        Spawns a Task waiting on all elements.

        Equations
        Instances For
          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 α))
          Equations
          Instances For