stream: def or structure?

Stream: general

[Yury G. Kudryashov]

I see that docs#stream API prefers stream.nth over application. Should it be a structure?

structure stream (α : Type*) := (nth : nat → α)

[Yury G. Kudryashov]

This will make some things a bit harder but without this the definitional equality s.nth n = s n will come out of definitions/lemmas, and it will be hard to have a simp normal form.

[Gabriel Ebner]

I think that's a good idea, just like set should be a structure.

[Eric Wieser]

I think the eta(?)-reduction arguments for keeping set as is probably don't apply to stream since stream is just not used very much.