Documentation

Lean.Server.AsyncList

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

source
instance IO.AsyncList.instInhabitedAsyncList {ε : Type u_1} {α : Type u_2} :
Inhabited (IO.AsyncList ε α)
Equations
  • IO.AsyncList.instInhabitedAsyncList = { default := IO.AsyncList.nil }
source
partial def IO.AsyncList.append {ε : Type u_1} {α : Type u_2} :
IO.AsyncList ε α → IO.AsyncList ε α → IO.AsyncList ε α
source
instance IO.AsyncList.instAppendAsyncList {ε : Type u_1} {α : Type u_2} :
Append (IO.AsyncList ε α)
Equations
  • IO.AsyncList.instAppendAsyncList = { append := IO.AsyncList.append }
source
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
source
instance IO.AsyncList.instCoeListAsyncList {α : Type u_1} {ε : Type u_2} :
Coe (List α) (IO.AsyncList ε α)
Equations
  • IO.AsyncList.instCoeListAsyncList = { coe := IO.AsyncList.ofList }
source
def IO.AsyncList.unfoldAsync {σ : Type} {ε : Type} {α : Type} (f : StateT σ (EIO ε) (Option α)) (init : σ) :
BaseIO (IO.AsyncList ε α)

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
source
partial def IO.AsyncList.unfoldAsync.step {σ : Type} {ε : Type} {α : Type} (f : StateT σ (EIO ε) (Option α)) (s : σ) :
EIO ε (IO.AsyncList ε α)
source
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.

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

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

source
partial def IO.AsyncList.waitFind? {α : Type} {ε : Type} (p : α → Bool) :
IO.AsyncList ε α → BaseIO (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.

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

source
def IO.AsyncList.waitHead? {ε : Type} {α : Type} (as : IO.AsyncList ε α) :
BaseIO (Task (Except ε (Option α)))
Equations