Skip to content

Conversation

Yosuke-Ito-345
Copy link
Contributor

Motivation for this change

fixes #1572

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@Yosuke-Ito-345
Copy link
Contributor Author

The errors appear to be due to technical issues. Can I ignore them?

@Yosuke-Ito-345 Yosuke-Ito-345 changed the title Generalize Codomain of Cumulative Make cdf an instance of Cumulative (fix #1572) Jul 13, 2025
@affeldt-aist
Copy link
Member

The errors appear to be due to technical issues. Can I ignore them?

They indeed look like elpi related, let us just ping @gares (who certainly already knows)

@Yosuke-Ito-345
Copy link
Contributor Author

Thank you for the review!

@affeldt-aist affeldt-aist force-pushed the generalize_cumulative branch from 3043ddc to 6661aa2 Compare August 23, 2025 08:09
@affeldt-aist affeldt-aist added this to the 1.14.0 milestone Aug 23, 2025
@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Aug 23, 2025
Copy link
Member

@affeldt-aist affeldt-aist left a comment

Choose a reason for hiding this comment

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

In the last commit, I have essentially shortened a proof by using an existing lemma and renamed a lemma using the ltgt substring that is often used when a lemma refers to both < and >.

@affeldt-aist affeldt-aist merged commit 93dfefc into math-comp:master Aug 23, 2025
67 checks passed
@Yosuke-Ito-345
Copy link
Contributor Author

Thank you for the review and the merge.

@Yosuke-Ito-345 Yosuke-Ito-345 deleted the generalize_cumulative branch August 24, 2025 06:57
hoheinzollern pushed a commit to hoheinzollern/analysis that referenced this pull request Sep 22, 2025
…p#1686)

* generalize cumulative

---------

Co-authored-by: Reynald Affeldt <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement ✨ This issue/PR is about adding new features enhancing the library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

make cdf an instance of Cumulative

2 participants