Skip to content

[Draft] Add extended real numbers#1338

Draft
CohenCyril wants to merge 4 commits into
math-comp:masterfrom
CohenCyril:numext
Draft

[Draft] Add extended real numbers#1338
CohenCyril wants to merge 4 commits into
math-comp:masterfrom
CohenCyril:numext

Conversation

@CohenCyril

@CohenCyril CohenCyril commented Feb 5, 2025 •
edited by proux01
Loading

Copy link
Copy Markdown
Member

Depends on #1520 (merged)

Motivation for this change
Minimal TODO list
  • added changelog entries with doc/changelog/make-entry.sh
  • SemiPseudoNormed (c.f. last commit)
  • adapt mathcomp analysis, note that lee_dsum_nneg_subfset, lee_dsum_npos_subfset, lee_sum_nneg_subfset, lee_sum_npos_subfset cannot be ported here.
  • backport numext lemmas about Z-modules to zmodext,
  • added corresponding documentation in the headers
  • tried to abide by the contribution guide
  • this PR contains an optimum number of meaningful commits

See this Checklist for details.

Automatic note to reviewers

Read this Checklist.

@CohenCyril CohenCyril marked this pull request as draft February 5, 2025 10:18
@CohenCyril CohenCyril force-pushed the numext branch 2 times, most recently from d0e667d to 2ed32e0 Compare February 10, 2025 23:40
proux01
proux01 reviewed Feb 13, 2025
View reviewed changes
Comment thread boot/eqtype.v Outdated
@proux01

proux01 commented Mar 6, 2025

Copy link
Copy Markdown
Contributor

Rebased on top of #1352

@proux01

proux01 commented Mar 10, 2025

Copy link
Copy Markdown
Contributor

Split into smaller commits to ease future review

@proux01 proux01 mentioned this pull request May 1, 2025
Merged
@proux01 proux01 changed the title [Draft] Splitting ssrnum and adding ordered zmodules [Draft] Adding ordered zmodules and extended real numbers Nov 26, 2025
@proux01 proux01 force-pushed the numext branch 3 times, most recently from 81e838a to 306c966 Compare November 27, 2025 14:04
@coqbot-app coqbot-app Bot added the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Nov 27, 2025
@coqbot-app coqbot-app Bot removed the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Nov 27, 2025
@proux01 proux01 force-pushed the numext branch 2 times, most recently from d10f53e to 81ad327 Compare November 28, 2025 10:50
@t6s

t6s commented Nov 28, 2025

Copy link
Copy Markdown
Member

this PR looks interesting as a starting point for doing Hahn embedding theorem

pi8027
pi8027 reviewed Nov 29, 2025
View reviewed changes
Comment thread algebra/interval.v Outdated
@pi8027 pi8027 mentioned this pull request Nov 30, 2025
Closed
2 tasks
pi8027
pi8027 reviewed Dec 1, 2025
View reviewed changes

@pi8027 pi8027 left a comment •
edited
Loading

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

While I know that the PR is not ready for review, I have a few more questions below.

If you split the PR into the draft part (the last two commits?) and the rest, I'm willing to review the latter. (No hurry.)

Comment thread algebra/num_theory/ssrnum.v Outdated
Comment thread algebra/Make
@pi8027 pi8027 mentioned this pull request Jan 2, 2026
Merged
4 tasks
@CohenCyril

CohenCyril commented Jan 8, 2026

Copy link
Copy Markdown
Member Author

I rebased!

@proux01

proux01 commented Jan 12, 2026

Copy link
Copy Markdown
Contributor

Aaaaargh, we've lost the commit history, what happened here?

@pi8027

pi8027 commented Jan 12, 2026

Copy link
Copy Markdown
Member

@proux01 It looks like Cyril squashed the commits. You can probably still retrieve your work: 81ad327.

@proux01 proux01 mentioned this pull request Jan 13, 2026
Merged
4 tasks
@proux01

proux01 commented Jan 14, 2026

Copy link
Copy Markdown
Contributor

Indeed, I retrieved the individual commits (without loosing Cyril's rebase, it was a pain) and split the PR in to three:

@proux01 proux01 changed the title [Draft] Adding ordered zmodules and extended real numbers [Draft] Add extended real numbers Jan 14, 2026
@proux01 proux01 mentioned this pull request Jan 14, 2026
Merged
4 tasks
@proux01 proux01 force-pushed the numext branch 2 times, most recently from 754f192 to 5cec398 Compare January 14, 2026 15:01
@CohenCyril CohenCyril mentioned this pull request Jan 14, 2026
Merged
4 tasks
@coqbot-app coqbot-app Bot added the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Jan 15, 2026
@coqbot-app coqbot-app Bot removed the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Jan 15, 2026
@proux01 proux01 force-pushed the numext branch 2 times, most recently from e208e2c to f07bac1 Compare January 16, 2026 08:57
@proux01 proux01 added the needs: merge of dependencies PR that depends on another. Documented in the original post of the PR. Review only the increment. label Jan 16, 2026
@proux01 proux01 added this to the 2.6.0 milestone Jan 16, 2026
@proux01 proux01 removed the needs: merge of dependencies PR that depends on another. Documented in the original post of the PR. Review only the increment. label Jan 16, 2026
@proux01 proux01 modified the milestones: 2.6.0, 2.7.0 May 11, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@pi8027 pi8027 pi8027 left review comments

@proux01 proux01 proux01 left review comments

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

2.7.0

Development

Successfully merging this pull request may close these issues.

4 participants

@CohenCyril @proux01 @t6s @pi8027