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

lim_sup -> limn_sup #1051

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

lim_sup -> limn_sup #1051

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

Comments

@affeldt-aist
Copy link
Member

analysis/theories/sequences.v

Line 2152 in 9fbd7cd

Definition lim_sup u := lim (sups u).

Would it be ok to rename lim_sup to limn_sup?
I am asking because there are "lim_sup" lemmas for realType in the pipeline
and it might be better to name these ones lim_sup (and not, say, limr_sup).
This also corresponds to the limn naming that the HB version of MathComp-Analysis is using.
Of course, a more unified mechanism would be better but that's another story for a bit later.
@affeldt-aist affeldt-aist added the question ❓ There is an unanswered question here label Oct 6, 2023
@affeldt-aist affeldt-aist added this to the 0.6.6 milestone Oct 6, 2023
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Oct 23, 2023
@affeldt-aist
fixes math-comp#1051
5565787
@affeldt-aist affeldt-aist mentioned this issue Oct 23, 2023
Merged
3 tasks
affeldt-aist added a commit that referenced this issue Oct 30, 2023
@affeldt-aist
fixes #1051 (rename lim_sup -> limn_sup) (#1068)
270c4c4 
* fixes #1051

* add only parsing
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Nov 10, 2023
@affeldt-aist
fixes math-comp#1051 (rename lim_sup -> limn_sup) (math-comp#1068)
746dbb3 
* fixes math-comp#1051

* add only parsing
proux01 pushed a commit that referenced this issue Nov 10, 2023
@affeldt-aist @proux01
fixes #1051 (rename lim_sup -> limn_sup) (#1068)
7e0b61e 
* fixes #1051

* add only parsing
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 #1051 (rename lim_sup -> limn_sup) affeldt-aist/analysis
1 participant
@affeldt-aist