Zulip Chat Archive

Stream: mathlib4

Topic: Bikeshedding: Data.Seq.Seq


Arien Malec (Jan 24 2023 at 06:55):

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 (Jan 24 2023 at 06:57):

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

Johan Commelin (Jan 24 2023 at 06:57):

Looks like it will.

Johan Commelin (Jan 24 2023 at 06:58):

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

Arien Malec (Jan 24 2023 at 07:01):

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 (Jan 24 2023 at 07:02):

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

Johan Commelin (Jan 24 2023 at 07:03):

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 (Jan 24 2023 at 09:15):

Stream.Seq could be a reasonable name?

Eric Wieser (Jan 24 2023 at 09:16):

(personally I think we should backport that first)

Johan Commelin (Jan 24 2023 at 09:16):

It's just a name change!

Johan Commelin (Jan 24 2023 at 09:16):

#align can take care of that

Eric Wieser (Jan 24 2023 at 09:17):

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

Johan Commelin (Jan 24 2023 at 09:18):

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

Eric Wieser (Jan 24 2023 at 09:19):

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 (Jan 25 2023 at 00:27):

mathlib#18284

Arien Malec (Feb 09 2023 at 17:10):

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


Last updated: Dec 20 2023 at 11:08 UTC