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.instInhabited {ε : Type u_1} {α : Type u_2} :
    Equations
      def IO.AsyncList.ofList {α : Type u_1} {ε : Type u_2} :
      List αAsyncList ε α
      Equations
        Instances For
          instance IO.AsyncList.instCoeList {α : Type u_1} {ε : Type u_2} :
          Coe (List α) (AsyncList ε α)
          Equations
            partial def IO.AsyncList.waitUntil {α : Type u_1} {ε : Type u_2} (p : αBool) :

            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} :

            Spawns a Task waiting on all elements.

            Equations
              Instances For
                partial def IO.AsyncList.waitFind? {α : Type u_1} {ε : Type u_2} (p : αBool) :

                Spawns a Task acting like List.find? but which will wait for tail evaluation 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} :
                AsyncList ε αBaseIO (List α × Option ε × Bool)

                Retrieve the already-computed prefix of the list. If computation has finished with an error, return it as well. The returned boolean indicates whether the complete AsyncList was returned, or whether only a proper prefix was returned.

                def IO.AsyncList.getFinishedPrefixWithTimeout {ε α : Type} (xs : AsyncList ε α) (timeoutMs : UInt32) (cancelTks : List (Lean.Server.ServerTask Unit) := []) :
                Equations
                  Instances For
                    partial def IO.AsyncList.getFinishedPrefixWithTimeout.go {ε α : Type} (cancelTks : List (Lean.Server.ServerTask Unit) := []) (timeoutTask : Lean.Server.ServerTask (Unit Except ε (AsyncList ε α))) (xs : AsyncList ε α) :
                    Equations
                      Instances For