stream.take vs stream.approx

Stream: general

[Yury G. Kudryashov]

Am I right that docs#stream.take is propositionally equal to docs#stream.approx? Should we leave only one of them?

[Kyle Miller]

They seem to be propositionally equal to me, with docs#stream.approx having better definitional equalities.

[Yury G. Kudryashov]

I'm going to move stream from lean core to mathlib so that we can fix names/docs/simp attrs.

[Kyle Miller]

Here's a crude proof to back up the claim:

import data.stream.basic

variables {α : Type*}

lemma foo {α : Type*} (n : ℕ) (s : stream α) : s.approx n = s.take n :=
begin
  rw [stream.take, list.range_eq_range'],
  induction n with n ih generalizing s,
  { refl },
  { rw [stream.approx, ih, list.range', list.map],
    congr' 1,
    rw [stream.tail, ←list.map_map],
    congr' 1,
    convert list.map_add_range' 1 _ _ using 2,
    ext,
    apply add_comm, },
end