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.

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

feat: merging functions on List + mergeSort #763

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Conversation

digama0
Copy link
Member

@digama0 digama0 commented Apr 23, 2024

Complement to #762. Adds List version of all the definitions in Data.Array.Merge. Also adds List.mergeSort (upstreamed from mathlib), as a replacement for Array.qsort on lists (because qsort cannot easily be expressed as is).

@digama0 digama0 added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Apr 23, 2024
(i.e. for all `x`, `y`, `y'`, `z`, if `x < y < z` and `x < y' < z` then `x < merge y y' < z`)
then the resulting list is again sorted.
-/
def mergeDedupWith [Ord α] (merge : α → α → α) : (xs ys : List α) → List α
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The merge parameter is a bit confusing. How about dedup, join or meld?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

combine?

Copy link
Member Author

@digama0 digama0 Apr 24, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

or just f. I think most of the other list functions don't give their predicate and function arguments long names, and while there are some downsides to having lots of one letter variables in context, one upside is that it makes it visibly distinct from global definitions. I assume that's the reason you flagged merge as being a bad name...

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, the issue is that merge clashes with a definition in this file. I'm happy with f, combine or whatever you decide.

Std/Data/List/Basic.lean Outdated Show resolved Hide resolved
Co-authored-by: François G. Dorais <[email protected]>
@kim-em kim-em added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Apr 30, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Apr 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author Waiting for PR author to address issues merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants