Documentation

Lean.Server.AsyncList

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

Type (max u v)

cons: {ε : Type u} → {α : Type v} → α → IO.AsyncList ε α → IO.AsyncList ε α
asyncTail: {ε : Type u} → {α : Type v} → Task (Except ε (IO.AsyncList ε α)) → IO.AsyncList ε α
nil: {ε : Type u} → {α : Type v} → IO.AsyncList ε α

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

Inhabited (IO.AsyncList ε α)

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

Append (IO.AsyncList ε α)

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

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 : σ) :

BaseIO (IO.AsyncList ε α)

Equations

IO.AsyncList.unfoldAsync f init = (fun step => do let tInit ← EIO.asTask (step init) Task.Priority.default pure (IO.AsyncList.asyncTail tInit)) (IO.AsyncList.unfoldAsync.step f)

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 ε

partial def IO.AsyncList.waitAll {α : Type} {ε : Type} (p : optParam (α → Bool) fun x => true) :

IO.AsyncList ε α → BaseIO (Task (List α × Option ε))

partial def IO.AsyncList.waitFind? {α : Type} {ε : Type} (p : α → Bool) :

IO.AsyncList ε α → BaseIO (Task (Except ε (Option α)))

partial def IO.AsyncList.updateFinishedPrefix {ε : Type} {α : Type} :

IO.AsyncList ε α → BaseIO (IO.AsyncList ε α × Option ε)

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

IO.AsyncList ε α → List α

Equations

IO.AsyncList.finishedPrefix = List.reverse ∘ IO.AsyncList.finishedPrefixAux []