Zulip Chat Archive

Stream: mathlib4

Topic: list.repeat

Reid Barton (Dec 22 2022 at 14:36):

Shouldn't docs#list.repeat be aligned to docs4#List.replicate ?

Mario Carneiro (Dec 22 2022 at 15:05):

I did that in the Data.List.Basic PR

Johan Commelin (Dec 22 2022 at 15:07):

but where?

Mario Carneiro (Dec 22 2022 at 15:10):

https://github.com/leanprover-community/mathlib4/compare/master...Data.List.Basic#diff-24cd7b4c58b3dc50f8820910fa58c62f5143f72bb58d263387126354a6b7008a

Reid Barton (Dec 22 2022 at 15:11):

https://github.com/leanprover-community/mathlib4/pull/966/files#diff-24cd7b4c58b3dc50f8820910fa58c62f5143f72bb58d263387126354a6b7008aR54-R56

Mario Carneiro (Dec 22 2022 at 15:11):

ah right, it's not actually an #align, it's a redefinition + deprecation

Mario Carneiro (Dec 22 2022 at 15:11):

because the argument order is different

Mario Carneiro (Dec 22 2022 at 15:12):

But maybe it should just be an #align (with \_x) to avoid the churn of all the downstream deprecations

Reid Barton (Dec 22 2022 at 15:13):

Currently there are a bunch of lemmas about replicate without #align

Mario Carneiro (Dec 22 2022 at 15:13):

for the same reason

Mario Carneiro (Dec 22 2022 at 15:14):

the functions about repeat are #aligned but also deprecated and the deprecation points you to the corresponding replicate theorem

Mario Carneiro (Dec 22 2022 at 15:15):

and I'm thinking now that if find/replace is really what we want then it should probably be an #align instead, even though this will generally break theorem statements

Mario Carneiro (Dec 22 2022 at 15:16):

alternatively we could backport change the argument order

Eric Wieser (Dec 22 2022 at 15:31):

Backporting seems reasonable to me

Reid Barton (Dec 22 2022 at 15:46):

I can't imagine there are very many uses of list.repeat in the first place

Martin Dvořák (Dec 22 2022 at 16:34):

Reid Barton said:

I can't imagine there are very many uses of list.repeat in the first place

My project contains 432 uses of list.repeat and I am surprised it is so many.

Yury G. Kudryashov (Jan 16 2023 at 07:10):

Mathlib 3 migrated to docs#list.replicate in #18127. A follow-up cleanup #18181 and a Mathlib 4 mathlib4#1579 that drops List.repeat are awaiting review.

Johan Commelin (Jan 16 2023 at 07:11):

Johan Commelin (Jan 16 2023 at 07:13):

I kicked the ml3 PR on the queue

Johan Commelin (Jan 16 2023 at 07:14):

@Yury G. Kudryashov Do you have plans to do that same with multiset.repeat?

Yury G. Kudryashov (Jan 16 2023 at 07:14):

No, I don't. Because docs#multiset.repeat is gone in #18127, meet docs#multiset.replicate.

Yury G. Kudryashov (Jan 16 2023 at 07:15):

UPD: no, I'm wrong.

Yury G. Kudryashov (Jan 16 2023 at 07:15):

I was sure that it's gone. Let me check.

Yury G. Kudryashov (Jan 16 2023 at 07:16):

It is gone; we have outdated docs.

Johan Commelin (Jan 16 2023 at 07:16):

Ooh, you did both at once! Great!

Yury G. Kudryashov (Jan 16 2023 at 07:17):

Also vector.repeat

Yury G. Kudryashov (Jan 16 2023 at 07:17):

I should've mentioned this in the commit message.

Johan Commelin (Jan 16 2023 at 07:18):

That'll make Mario happy :grinning:

Mario Carneiro (Jan 16 2023 at 07:18):

I pressed the merge button :)

Eric Wieser (Jan 16 2023 at 10:48):

~~I just added docs#fin.repeat...~~ nevermind, that has different semantics

Last updated: Dec 20 2023 at 11:08 UTC