Init.Data.Stream

source

class ToStream (collection : Type u) (stream : outParam (Type u)) :

Type u

toStream : collection → stream

Instances

source

class Stream (stream : Type u) (value : outParam (Type v)) :

Type (max u v)

next? : stream → Option (value × stream)

Instances

source

def Stream.forIn {ρ : Type u_1} {α : Type u_2} {m : Type u_3 → Type u_4} {β : Type u_3} [inst : Stream ρ α] [inst : Monad m] (s : ρ) (b : β) (f : α → β → m (ForInStep β)) :

m β

Equations

Stream.forIn s b f = let _ := { default := pure b }; Stream.forIn.visit f s b

source

partial def Stream.forIn.visit {ρ : Type u_1} {α : Type u_2} {m : Type u_3 → Type u_4} {β : Type u_3} [inst : Stream ρ α] [inst : Monad m] (f : α → β → m (ForInStep β)) (s : ρ) (b : β) :

m β

source

instance instForIn {ρ : Type u_1} {α : Type u_2} {m : Type u_3 → Type u_4} [inst : Stream ρ α] :

ForIn m ρ α

Equations

instForIn = { forIn := fun {β} [Monad m] => Stream.forIn }

source

instance instToStreamList {α : Type u_1} :

ToStream (List α) (List α)

Equations

instToStreamList = { toStream := fun c => c }

source

instance instToStreamArraySubarray {α : Type u_1} :

ToStream (Array α) (Subarray α)

Equations

instToStreamArraySubarray = { toStream := fun a => Array.toSubarray a 0 (Array.size a) }

source

instance instToStreamSubarray {α : Type u_1} :

ToStream (Subarray α) (Subarray α)

Equations

instToStreamSubarray = { toStream := fun a => a }

source

instance instToStreamStringSubstring:

ToStream String Substring

Equations

instToStreamStringSubstring = { toStream := fun s => String.toSubstring s }

source

instance instToStreamRange:

ToStream Std.Range Std.Range

Equations

instToStreamRange = { toStream := fun r => r }

source

instance instStreamProdProd {ρ : Type u_1} {α : Type u_2} {γ : Type u_3} {β : Type u_4} [inst : Stream ρ α] [inst : Stream γ β] :

Stream (ρ × γ) (α × β)

Equations

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

source

instance instStreamList {α : Type u_1} :

Stream (List α) α

Equations

instStreamList = { next? := fun x => match x with | [] => none | a :: as => some (a, as) }

source

instance instStreamSubarray {α : Type u_1} :

Stream (Subarray α) α

Equations

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

source

instance instStreamRangeNat:

Stream Std.Range Nat

Equations

instStreamRangeNat = { next? := fun r => if r.start < r.stop then some (r.start, { start := r.start + r.step, stop := r.stop, step := r.step }) else none }

source

instance instStreamSubstringChar:

Stream Substring Char

Equations

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