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

Drop up to n values from the stream s.

Equations

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

def Std.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

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

@[simp]

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

theorem Std.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 Std.Stream.snd_take_eq_drop {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) (n : Nat) : (take s n).snd = drop s n

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

Tail recursive version of Stream.take.

Equations

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

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

Inner loop for Stream.takeTR.

Equations

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

theorem Std.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 Std.Stream.fst_takeTR {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) (n : Nat) : (takeTR s n).fst = (take s n).fst

theorem Std.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 Std.Stream.snd_takeTR {σ : Type u_1} {α : Type u_2} [Stream σ α] (s : σ) (n : Nat) : (takeTR s n).snd = drop s n

@[csimp]

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

@[simp]

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

@[simp]

theorem Std.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)