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

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

Instances For

source

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

Inhabited (AsyncList ε α)

Equations

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

source

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

List α → AsyncList ε α

Equations

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

Instances For

source

instance IO.AsyncList.instCoeList {α : Type u_1} {ε : Type u_2} :

Coe (List α) (AsyncList ε α)

Equations

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

source

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.

source

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

Instances For

source

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.

source

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.

source