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

Add a number notation for ring #841

Merged
merged 5 commits into from Mar 4, 2022
Merged

Add a number notation for ring #841

merged 5 commits into from Mar 4, 2022

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Jan 15, 2022 •
edited

Now, 12 or 42 are read as 12%:R or 42%:R in scope ring_scope.
If ssrint is imported, -6 is read as (-6)%:~R.

One may have to add a few %nat in code that was using concrete
nat values in scope ring_scope.

Overlays (to be merged before merging current PR)
Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries)
  • added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

@proux01 proux01 mentioned this pull request Jan 15, 2022
Merged
4 tasks
proux01 added a commit to coq-community/gaia that referenced this pull request Jan 16, 2022
@proux01
Add %nat for nat constants
de83948 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
@proux01 proux01 mentioned this pull request Jan 16, 2022
Merged
proux01 added a commit to proux01/real-closed that referenced this pull request Jan 16, 2022
@proux01
Add %nat for nat constant
4650aff 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
proux01 added a commit to proux01/real-closed that referenced this pull request Jan 16, 2022
@proux01
Add %N for nat constant
26f6c83 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
@proux01 proux01 mentioned this pull request Jan 16, 2022
Merged
@CohenCyril
Copy link
Member

The canonical way to refer to nat_scope in mathcomp is %N.

proux01 added a commit to coq-community/gaia that referenced this pull request Jan 16, 2022
@proux01
Add %N for nat constants
fdaec5e 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
proux01 added a commit to proux01/odd-order that referenced this pull request Jan 16, 2022
@proux01
Add %N for nat constants
343141f 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
@proux01 proux01 mentioned this pull request Jan 16, 2022
Merged
proux01 added a commit to coq-community/gaia that referenced this pull request Jan 16, 2022
@proux01
Add %N for nat constants
aed8732 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
proux01 added a commit to proux01/odd-order that referenced this pull request Jan 17, 2022
@proux01
Add %N for nat constants
8c2b34b 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
@proux01 proux01 marked this pull request as draft January 22, 2022 09:31
proux01 added a commit to proux01/CoqEAL that referenced this pull request Jan 22, 2022
@proux01
Add %N for nat constants
24576b6 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
This was referenced Jan 22, 2022
Merged
Merged
proux01 added a commit to proux01/analysis that referenced this pull request Jan 22, 2022
@proux01
Add %N for nat constants
9fdc694 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
@proux01 proux01 mentioned this pull request Jan 22, 2022
Merged
proux01 added a commit to proux01/fourcolor that referenced this pull request Jan 22, 2022
@proux01
Add %N for nat constants
9cc1bbb 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).  Add %N for nat constants
@proux01 proux01 mentioned this pull request Jan 22, 2022
Merged
affeldt-aist pushed a commit to math-comp/analysis that referenced this pull request Jan 24, 2022
@proux01 @affeldt-aist
Add %N for nat constants
7a82f0d 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
@CohenCyril CohenCyril mentioned this pull request Jan 25, 2022
Merged
5 tasks
@proux01
Copy link
Contributor Author

proux01 commented Jan 26, 2022

@gares you were right, the Open Scope ring_scope in extraspecial.v and extremal.v were not needed

@chdoc FYI:

  • 22 additional %N
  • 21 %:R removed

so almost on par now (thanks to Enrico)

proux01 added a commit to proux01/fourcolor that referenced this pull request Feb 14, 2022
@proux01
Add %N for nat constants
a1d9ca2 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).  Add %N for nat constants
proux01 added a commit to proux01/odd-order that referenced this pull request Feb 14, 2022
@proux01
Add %N for nat constants
633305c 
This is in preparation of
math-comp/math-comp#841

This is backward compatible (it only ensures that natural number
constants will kee being interpreted in nat_scope when a number
notation will be added in ring_scope).
@proux01 proux01 force-pushed the ring-number-notation branch 2 times, most recently from 255bdc6 to 1ec8a76 Compare February 16, 2022 09:10
@proux01 proux01 marked this pull request as ready for review February 17, 2022 08:31
@proux01
Copy link
Contributor Author

proux01 commented Feb 17, 2022

Rebased, all overlays merged, this will be mergeable whenever we decide to drop support for Coq 8.11 and 8.12.

@proux01 proux01 mentioned this pull request Feb 17, 2022
Merged
3 tasks
@proux01 proux01 mentioned this pull request Mar 2, 2022
Merged
CohenCyril
CohenCyril approved these changes Mar 3, 2022
View reviewed changes
Copy link
Member

@CohenCyril CohenCyril left a comment

Choose a reason for hiding this comment

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

Rebase and merge?

@proux01
[CI] Update Nix CI
cdcfada
@proux01
Add a number notation in AC_scope
8b34f31
@proux01
Add %N for natural numbers
15012fb 
This is done in preparation to the addition of a number notation in
scope ring_scope. So we want to avoid natural number constants such as
2 or 3 to be interpreted in ring_scope.
@proux01
Add a number notation for ring
3bee1da 
Now, 12 or 42 are read as 12%:R or 42%:R in scope ring_scope.
If ssrint is imported, -6 is read as (-6)%:~R.

One may have to add a few %N in code that was using concrete
nat values in scope ring_scope.
@proux01
Remove useless %:R on numbers
dd6532a 
2 is now a notation for 2%:R
@proux01 proux01 merged commit 5477050 into math-comp:master Mar 4, 2022
@proux01 proux01 deleted the ring-number-notation branch March 4, 2022 07:28
@proux01
Copy link
Contributor Author

proux01 commented Mar 4, 2022

done

@proux01 proux01 mentioned this pull request Mar 18, 2022
Merged
5 tasks
pi8027 added a commit to math-comp/algebra-tactics that referenced this pull request Mar 31, 2022
@pi8027
Compatibility with math-comp/math-comp#841
48ae6f0
pi8027 added a commit to math-comp/algebra-tactics that referenced this pull request Mar 31, 2022
@pi8027
Merge pull request #50 from math-comp/number-notation
3cc388f 
Compatibility with math-comp/math-comp#841
@pi8027 pi8027 mentioned this pull request Mar 31, 2022
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CohenCyril CohenCyril CohenCyril approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@proux01 @CohenCyril