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 `Stream`s in monadic code.

source
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

Instances

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

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

Instances

source
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

Instances For

source
@[instance 100]
instance Std.instForInOfStream {ρ : Type u_1} {α : Type u_2} {m : Type u_3 → Type u_4} [Stream ρ α] :
ForIn m ρ α
Equations

- Std.instForInOfStream = { forIn := fun {β : Type ?u.24} [Monad m] => Std.Stream.forIn }

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

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

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

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

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

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

source
instance Std.instToStreamStringSubstring :
ToStream String Substring
Equations

- Std.instToStreamStringSubstring = { toStream := fun (s : String) => s.toSubstring }

source
instance Std.instToStreamRange :
ToStream Range Range
Equations

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

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

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

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

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

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

source
instance Std.instStreamRangeNat :
Stream Range Nat
Equations

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

source
@[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

Instances For

source
@[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?

Instances For

source
@[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

Instances For

source
@[reducible, inline]
abbrev ToStream.toStream {collection : Type u} {stream : outParam (Type u)} [self : Std.ToStream collection stream] :
collection → stream
Equations

- ToStream.toStream = Std.toStream

Instances For