Remark: we considered using the following alternative design

structure Stream (α : Type u) where
  stream : Type u
  next? : stream → Option (α × stream)

class ToStream (collection : Type u) (value : outParam (Type v)) where
  toStream : collection → Stream value

where Stream is not a class, and its state is encapsulated. The key problem is that the type Stream α "lives" in a universe higher than α. This is a problem because we want to use Streams in monadic code.

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

Streams are used to implement parallel for statements. Example:

for x in xs, y in ys do
  ...

is expanded into

let mut s := toStream ys
for x in xs do
  match Stream.next? s with
  | none => break
  | some (y, s') =>
    s := s'
    ...

• toStream : collection → stream

class Std.Stream (stream : Type u) (value : outParam (Type v)) : Type (max u v)

• next? : stream → Option (value × stream)

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

Equations

• Std.Stream.forIn s b f = Std.Stream.forIn.visit✝ f s b

@[instance_reducible, instance 100]

instance Std.instForInOfMonadOfStream {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_4} [Monad m] [Stream ρ α] : ForIn m ρ α

Equations

• Std.instForInOfMonadOfStream = { forIn := fun {β : Type ?u.4} => Std.Stream.forIn }

@[instance_reducible]

instance Std.instToStreamList {α : Type u_1} : ToStream (List α) (List α)

Equations

• Std.instToStreamList = { toStream := fun (c : List α) => c }

@[instance_reducible]

instance Std.instToStreamArraySubarray {α : Type u_1} : ToStream (Array α) (Subarray α)

Equations

• Std.instToStreamArraySubarray = { toStream := fun (a : Array α) => Std.Rii.Sliceable.mkSlice a *...* }

@[instance_reducible]

instance Std.instToStreamSubarray {α : Type u_1} : ToStream (Subarray α) (Subarray α)

Equations

• Std.instToStreamSubarray = { toStream := fun (a : Subarray α) => a }

@[instance_reducible]

instance Std.instToStreamStringRaw : ToStream String Substring.Raw

Equations

• Std.instToStreamStringRaw = { toStream := fun (s : String) => s.toRawSubstring }

@[instance_reducible]

instance Std.instToStreamRange : ToStream Legacy.Range Legacy.Range

Equations

• Std.instToStreamRange = { toStream := fun (r : Std.Legacy.Range) => r }

@[instance_reducible]

instance Std.instStreamProd {ρ : Type u_1} {α : Type u_2} {γ : Type u_3} {β : Type u_4} [Stream ρ α] [Stream γ β] : Stream (ρ × γ) (α × β)

Equations

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

@[instance_reducible]

instance Std.instStreamList {α : Type u_1} : Stream (List α) α

Equations

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

@[instance_reducible]

instance Std.instStreamSubarray {α : Type u_1} : Stream (Subarray α) α

Equations

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

@[instance_reducible]

instance Std.instStreamRangeNat : Stream Legacy.Range Nat

Equations

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

@[reducible, inline, deprecated Std.Stream (since := "2025-10-01")]

abbrev Stream (stream : Type u_1) (value : outParam (Type u_2)) : Type (max u_1 u_2)

Equations

• Stream = Std.Stream

@[reducible, inline]

abbrev Stream.next? {stream : Type u} {value : outParam (Type v)} [self : Std.Stream stream value] : stream → Option (value × stream)

Equations

• Stream.next? = Std.Stream.next?

@[reducible, inline, deprecated Std.ToStream (since := "2025-10-01")]

abbrev ToStream (collection : Type u_1) (stream : outParam (Type u_1)) : Type u_1

Equations

• ToStream = Std.ToStream

@[reducible, inline]

abbrev ToStream.toStream {collection : Type u} {stream : outParam (Type u)} [self : Std.ToStream collection stream] : collection → stream

Equations

• ToStream.toStream = Std.toStream