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

ereal_nondecreasing_cvg -> ereal_nondecreasing_cvgn #1052

Closed
affeldt-aist opened this issue Oct 8, 2023 · 0 comments · Fixed by #1085
Closed

ereal_nondecreasing_cvg -> ereal_nondecreasing_cvgn #1052

affeldt-aist opened this issue Oct 8, 2023 · 0 comments · Fixed by #1085
Labels
question ❓ There is an unanswered question here
Milestone
0.6.6

Comments

@affeldt-aist
Copy link
Member

analysis/theories/sequences.v

Line 1462 in 9fbd7cd

Lemma ereal_nondecreasing_cvg (R : realType) (u_ : (\bar R)^nat) :

wouldn't is be better to rename
ereal_nondecreasing_cvg -> ereal_nondecreasing_cvgn
to make room for a forthcoming
ereal_nondecreasing_cvgr?

and to following the naming convention, ereal_nondecreasing_cvg could maybe be renamed nondecreasing_cvge
@affeldt-aist affeldt-aist added this to the 0.6.6 milestone Oct 8, 2023
@affeldt-aist affeldt-aist added the question ❓ There is an unanswered question here label Oct 8, 2023
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Nov 9, 2023
@affeldt-aist
fixes math-comp#1052
6c44bb5
@affeldt-aist affeldt-aist mentioned this issue Nov 9, 2023
Merged
3 tasks
affeldt-aist added a commit that referenced this issue Nov 10, 2023
@affeldt-aist
fixes #1052 (#1085)
34b4b0b
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Nov 14, 2023
@affeldt-aist
fixes math-comp#1052 (math-comp#1085)
7e5bd94
proux01 pushed a commit that referenced this issue Nov 15, 2023
@affeldt-aist @proux01
fixes #1052 (#1085)
31e13ee
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
question ❓ There is an unanswered question here
Projects
None yet
Milestone
0.6.6
Development

Successfully merging a pull request may close this issue.

fixes #1052 (renaming in sequences.v) affeldt-aist/analysis
1 participant
@affeldt-aist