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

Drop up to n values from the stream s.

Equations

• Stream.drop s 0 = s
• Stream.drop s n.succ = match Stream.next? s with | none => s | some (fst, s) => Stream.drop s n

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.

Equations

• Stream.take s 0 = ([], s)
• Stream.take s n.succ = match Stream.next? s with | none => ([], s) | some (a, s) => match Stream.take s n with | (as, s) => (a :: as, s)

@[simp]

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

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

@[simp]

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

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

Tail recursive version of Stream.take.

Equations

• Stream.takeTR s n = Stream.takeTR.loop s [] n

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

Inner loop for Stream.takeTR.

Equations

• Stream.takeTR.loop s acc 0 = (acc.reverse, s)
• Stream.takeTR.loop s acc n.succ = match Stream.next? s with | none => (acc.reverse, s) | some (a, s) => Stream.takeTR.loop s (a :: acc) n

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

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

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

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

@[csimp]

theorem Stream.take_eq_takeTR : @Stream.take = @Stream.takeTR

@[simp]

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

@[simp]

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