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 ε.

• cons {ε : Type u} {α : Type v} (hd : α) (tl : AsyncList ε α) : AsyncList ε α
• delayed {ε : Type u} {α : Type v} (tl : Lean.Server.ServerTask (Except ε (AsyncList ε α))) : AsyncList ε α
• nil {ε : Type u} {α : Type v} : AsyncList ε α

instance IO.AsyncList.instInhabited {ε : Type u_1} {α : Type u_2} : Inhabited (AsyncList ε α)

Equations

• IO.AsyncList.instInhabited = { default := IO.AsyncList.nil }

def IO.AsyncList.ofList {α : Type u_1} {ε : Type u_2} : List α → AsyncList ε α

Equations

• IO.AsyncList.ofList = List.foldr IO.AsyncList.cons IO.AsyncList.nil

instance IO.AsyncList.instCoeList {α : Type u_1} {ε : Type u_2} : Coe (List α) (AsyncList ε α)

Equations

• IO.AsyncList.instCoeList = { coe := IO.AsyncList.ofList }

partial def IO.AsyncList.waitUntil {α : Type u_1} {ε : Type u_2} (p : α → Bool) : AsyncList ε α → Lean.Server.ServerTask (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} : AsyncList ε α → Lean.Server.ServerTask (List α × Option ε)

Spawns a Task waiting on all elements.

Equations

• IO.AsyncList.waitAll = IO.AsyncList.waitUntil fun (x : α) => false

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

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) := []) : BaseIO (List α × Option ε × Bool)

Equations

• One or more equations did not get rendered due to their size.

partial def IO.AsyncList.getFinishedPrefixWithTimeout.go {ε α : Type} (cancelTks : List (Lean.Server.ServerTask Unit) := []) (timeoutTask : Lean.Server.ServerTask (Unit ⊕ Except ε (AsyncList ε α))) (xs : AsyncList ε α) : BaseIO (List α × Option ε × Bool)

def IO.AsyncList.getFinishedPrefixWithConsistentLatency {ε α : Type} (xs : AsyncList ε α) (latencyMs : UInt32) (cancelTks : List (Lean.Server.ServerTask Unit) := []) : BaseIO (List α × Option ε × Bool)

Equations

• One or more equations did not get rendered due to their size.

def IO.AsyncList.getFinishedPrefixWithConsistentLatency.sleepWithCancellation (cancelTks : List (Lean.Server.ServerTask Unit) := []) (sleepDurationMs : UInt32) : BaseIO Unit

Equations

• One or more equations did not get rendered due to their size.