Documentation

Init.Data.Stream

class ToStream (collection : Type u) (stream : outParam (Type u)) :
Type u
  • toStream : collectionstream
Instances
class Stream (stream : Type u) (value : outParam (Type v)) :
Type (max u v)
  • next? : streamOption (value × stream)
Instances
def Stream.forIn {ρ : Type u_1} {α : Type u_2} {m : Type u_3Type u_4} {β : Type u_3} [inst : Stream ρ α] [inst : Monad m] (s : ρ) (b : β) (f : αβm (ForInStep β)) :
m β
Equations
partial def Stream.forIn.visit {ρ : Type u_1} {α : Type u_2} {m : Type u_3Type u_4} {β : Type u_3} [inst : Stream ρ α] [inst : Monad m] (f : αβm (ForInStep β)) (s : ρ) (b : β) :
m β
instance instForIn {ρ : Type u_1} {α : Type u_2} {m : Type u_3Type u_4} [inst : Stream ρ α] :
ForIn m ρ α
Equations
  • instForIn = { forIn := fun {β} [Monad m] => Stream.forIn }
instance instToStreamList {α : Type u_1} :
ToStream (List α) (List α)
Equations
  • instToStreamList = { toStream := fun c => c }
instance instToStreamArraySubarray {α : Type u_1} :
Equations
instance instToStreamSubarray {α : Type u_1} :
Equations
  • instToStreamSubarray = { toStream := fun a => a }
Equations
instance instStreamProdProd {ρ : Type u_1} {α : Type u_2} {γ : Type u_3} {β : Type u_4} [inst : Stream ρ α] [inst : Stream γ β] :
Stream (ρ × γ) (α × β)
Equations
  • instStreamProdProd = { next? := fun _fun_discr => match _fun_discr with | (s₁, s₂) => match Stream.next? s₁ with | none => none | some (a, s₁) => match Stream.next? s₂ with | none => none | some (b, s₂) => some ((a, b), s₁, s₂) }
instance instStreamList {α : Type u_1} :
Stream (List α) α
Equations
  • instStreamList = { next? := fun _fun_discr => match _fun_discr with | [] => none | a :: as => some (a, as) }
instance instStreamSubarray {α : Type u_1} :
Equations
  • instStreamSubarray = { next? := fun s => if h : s.start < s.stop then let_fun this := (_ : Nat.succ s.start s.stop); some (Array.get s.as { val := s.start, isLt := (_ : s.start < Array.size s.as) }, { as := s.as, start := s.start + 1, stop := s.stop, h₁ := this, h₂ := (_ : s.stop Array.size s.as) }) else none }
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 }
Equations