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):
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