data.stream.defs

Stream: mathlib4

[Eric Rodriguez]

(sorry for all the threadspam, I thought i'll keep all separate things separate)

This file should be easily portable, but there is already a docs4#Stream that is not like docs#stream, and so we need a new name for the Lean3 notion. What should we use?

[Mario Carneiro]

I thought there was already a #align stream Stream' somewhere. I've already used it several times as a canonical example of where we want to use an #align directive

[Eric Rodriguez]

neither synport nor control+f can seem to find it: https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Data/Stream/Defs.lean

[Eric Rodriguez]

i'll hand-align it tomorrow, then

[Eric Rodriguez]

what's docs#state gone to? mathport seems to think docs4#State which is a 404

[Mario Carneiro]

docs4#StateM I think