- toStream : collection → stream
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
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 β
Equations
- instToStreamArraySubarray = { toStream := fun a => Array.toSubarray a 0 (Array.size a) }
Equations
- instToStreamStringSubstring = { toStream := fun s => String.toSubstring s }
Equations
- instToStreamRange = { toStream := fun r => r }
instance
instStreamProdProd
{ρ : Type u_1}
{α : Type u_2}
{γ : Type u_3}
{β : Type u_4}
[inst : Stream ρ α]
[inst : 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₂) }
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
- instStreamSubstringChar = { next? := fun s => if s.startPos < s.stopPos then some (String.get s.str s.startPos, { str := s.str, startPos := String.next s.str s.startPos, stopPos := s.stopPos }) else none }