Zulip Chat Archive

Stream: general

Topic: stream: def or structure?

Yury G. Kudryashov (Oct 22 2021 at 23:39):

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

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

Yury G. Kudryashov (Oct 22 2021 at 23:40):

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 (Oct 25 2021 at 07:37):

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

Eric Wieser (Oct 25 2021 at 07:42):

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.

Last updated: Aug 03 2023 at 10:10 UTC