Skip to content

Generalize count_merge from eqType to Type #1174

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
Merged
proux01 merged 1 commit into from
Feb 17, 2024
Merged

Generalize count_merge from eqType to Type #1174

proux01 merged 1 commit into from
Feb 17, 2024

Conversation

@pi8027
Copy link
Member

@pi8027 pi8027 commented Feb 17, 2024

Motivation for this change

Lemma count_merge does not require an eqType. Thanks to this generalization, size_cat and perm_merge become immediate consequences of count_merge.

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • [ ] added corresponding documentation in the headers
  • tried to abide by the contribution guide
Compatibility with MathComp 1.X
  • I added the label TODO: MC-1 port to make sure someone ports this PR to
    the mathcomp-1 branch or I already opened an issue or PR (please cross reference).
Automatic note to reviewers

Read this Checklist and put a milestone if possible.
proux01
proux01 approved these changes Feb 17, 2024
View reviewed changes
Copy link
Contributor

@proux01 proux01 left a comment

Choose a reason for hiding this comment

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

Great
@proux01 proux01 merged commit 8a44e7a into master Feb 17, 2024
@proux01 proux01 deleted the count_merge branch February 17, 2024 18:03
@proux01 proux01 added this to the 2.3.0 milestone Apr 12, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

3 participants

@pi8027 @proux01