Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Rename Data.List.Properties.*-is-foldr #2516

Open
jamesmckinna opened this issue Dec 11, 2024 · 1 comment
Open

Rename Data.List.Properties.*-is-foldr #2516

jamesmckinna opened this issue Dec 11, 2024 · 1 comment
Labels
bikeshedding cosmetic deprecation library-design naming refactoring
Milestone
v3.0

Comments

@jamesmckinna
Copy link
Contributor

jamesmckinna commented Dec 11, 2024 •
edited
Loading

I wouldn't call this partition-is-foldr but partition-as-foldr , or partition-via-foldr. And yes, foldr being the List eliminator, we need to be careful to not have an explosion of these. Having said that, I'm fine with partition as it is an important function.

But we already have

  • id-is-foldr
  • -is-foldr
  • map-is-foldr
  • ...

So it does explode into a deprecation-fest if we follow your lead? v3.0?

Originally posted by @jamesmckinna in #2505 (comment)

Proposal: all *-is-fold* lemmas be renamed, and the old names deprecated.

Issue: what alternative naming policy?
@JacquesCarette JacquesCarette added this to the v3.0 milestone Dec 11, 2024
@MatthewDaggitt
Copy link
Contributor

So it does explode into a deprecation-fest if we follow your lead? v3.0?

Yes, there are lot of such names in the library. Personally my view is that the name isn't so bad that we need to go and deprecate it... but if other people are strongly in favour I'm happy to defer.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bikeshedding cosmetic deprecation library-design naming refactoring
Projects
None yet
Milestone
v3.0
Development

No branches or pull requests
3 participants
@JacquesCarette @MatthewDaggitt @jamesmckinna