def Stream.drop {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) : Nat → σ

Drop up to n values from the stream s.

def Stream.take {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) : Nat → List α × σ

Read up to n values from the stream s as a list from first to last.

@[simp]

theorem Stream.fst_take_zero {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) : (take s 0).fst = []

theorem Stream.fst_take_succ {σ : Type u_1} {α : Type u_2} {n : Nat} [Stream σ α] (s : σ) : (take s (n + 1)).fst = match next? s with | none => [] | some (a, s) => a :: (take s n).fst

@[simp]

theorem Stream.snd_take_eq_drop {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) (n : Nat) : (take s n).snd = drop s n

def Stream.takeTR {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) (n : Nat) : List α × σ

Tail recursive version of Stream.take.

def Stream.takeTR.loop {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) (acc : List α) : Nat → List α × σ

Inner loop for Stream.takeTR.

theorem Stream.fst_takeTR_loop {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) (acc : List α) (n : Nat) : (takeTR.loop s acc n).fst = acc.reverseAux (take s n).fst

theorem Stream.fst_takeTR {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) (n : Nat) : (takeTR s n).fst = (take s n).fst

theorem Stream.snd_takeTR_loop {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) (acc : List α) (n : Nat) : (takeTR.loop s acc n).snd = drop s n

theorem Stream.snd_takeTR {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) (n : Nat) : (takeTR s n).snd = drop s n

@[csimp]

theorem Stream.take_eq_takeTR : @take = @takeTR

@[simp]

theorem List.stream_drop_eq_drop {α : Type u_1} {n : Nat} (l : List α) : Stream.drop l n = drop n l

@[simp]

theorem List.stream_take_eq_take_drop {α : Type u_1} {n : Nat} (l : List α) : Stream.take l n = (take n l, drop n l)