Bikeshedding: Data.Seq.Seq

Stream: mathlib4

[Arien Malec]

Right now, Data.Seq clashes with the typeclass Seq (docs4#Seq) (used to be has_seq.

I've temporarily renamed this to Seq' but that's pretty awful and confusing.

Given the representation, Sequence might be the easiest name; Stream, which is what I'd think of it in other language contexts, is already taken....

[Johan Commelin]

Let's double check that this doesn't cause another clash down the road: docs#sequence

[Johan Commelin]

Looks like it will.

[Johan Commelin]

@Arien Malec Can you put the whole file in a namespace for now?

[Arien Malec]

Well in the PR (mathlib4#1808) I've currently got Seq' but yes, could revert back & wrap up in something. The nice thing, though, about Seq' is that it's pretty easy to mass replace...

[Johan Commelin]

Ok, if it already works, maybe leave it until we make a final decision

[Johan Commelin]

https://leanprover-community.github.io/mathlib-port-status/?q=seq suggests that there are only 15 files depending on this file. So it probably doesn't matter too much what we do, as long as it doesn't clash with other names in mathlib.

[Eric Wieser]

Stream.Seq could be a reasonable name?

[Eric Wieser]

(personally I think we should backport that first)

[Johan Commelin]

It's just a name change!

[Johan Commelin]

#align can take care of that

[Eric Wieser]

Not quite, it also is going to mean adding some namespace keywords

[Johan Commelin]

Yes, but that's a very minor thing. This file is barely used.

[Eric Wieser]

It's easier to review a mathlib 3 PR that adds a handful of namespace lines than a mathlib 4 PR that mixes changes with porting

[Arien Malec]

mathlib#18284

[Arien Malec]

Sending a ping to this thread -- nobody has touched the mathlib PR and my mathlib4 PR is currently going nowhere.