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

name: le0r_derive1_ndecr #1380

Open
affeldt-aist opened this issue Nov 5, 2024 · 2 comments
Open

name: le0r_derive1_ndecr #1380

affeldt-aist opened this issue Nov 5, 2024 · 2 comments
Labels
renaming/refactoring 🔧 This is about a renaming or refactoring in the library
Milestone
1.8.0

Comments

@affeldt-aist
Copy link
Member

analysis/theories/derive.v

Line 1623 in d26b17b

Lemma le0r_derive1_ndecr (R : realType) (f : R -> R) (a b : R) :

should maybe have been ge0r_derive1_ndecr
@affeldt-aist affeldt-aist added the renaming/refactoring 🔧 This is about a renaming or refactoring in the library label Nov 5, 2024
@affeldt-aist affeldt-aist added this to the 1.7.0 milestone Nov 5, 2024
@affeldt-aist
Copy link
Member Author

Moreover, there is a pending generalization -> postpone to 1.8.0

@affeldt-aist affeldt-aist modified the milestones: 1.7.0, 1.8.0 Nov 22, 2024
@affeldt-aist
Copy link
Member Author

@t6s there was actually an issue for what we discussed earlier today, you can close it with your forthcoming PR

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
renaming/refactoring 🔧 This is about a renaming or refactoring in the library
Projects
None yet
Milestone
1.8.0
Development

No branches or pull requests
1 participant
@affeldt-aist