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

mulr_rev out of forms.v #1122

Merged
merged 9 commits into from
Apr 24, 2024
Merged

mulr_rev out of forms.v #1122

merged 9 commits into from
Apr 24, 2024

Conversation

affeldt-aist
Copy link
Member

Motivation for this change

fixes #1092

mulr_rev had nothing to do in derive.v

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md

- [] added corresponding documentation in the headers

Compatibility with MathComp 2.0
  • I added the label TODO: HB port to make sure someone ports this PR to
    the hierarchy-builder branch or I already opened an issue or PR (please cross reference).
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@affeldt-aist affeldt-aist added the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Dec 21, 2023
@affeldt-aist affeldt-aist added this to the 0.6.7 milestone Dec 21, 2023
@affeldt-aist affeldt-aist force-pushed the fixes_1092 branch 2 times, most recently from 1ea61e4 to d1d4cb8 Compare December 21, 2023 12:54
@affeldt-aist
Copy link
Member Author

There is certainly something smarter to do with R^c.

@affeldt-aist affeldt-aist modified the milestones: 0.6.7, 0.6.8 Jan 8, 2024
@affeldt-aist
Copy link
Member Author

@CohenCyril Since you thumbs uped the corresponding you may have an interest in this PR. Otherwise, we'll postpone to 1.0.0.

@CohenCyril
Copy link
Member

@CohenCyril Since you thumbs uped the corresponding you may have an interest in this PR. Otherwise, we'll postpone to 1.0.0.

This should ultimately be backported to mathcomp, but there is no emergency here.

@affeldt-aist affeldt-aist modified the milestones: 0.7.0, 1.0.0, 1.0.1 Jan 18, 2024
@affeldt-aist affeldt-aist modified the milestones: 1.0.1, 1.1.0, 1.2.0 Mar 24, 2024
@affeldt-aist affeldt-aist removed the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Apr 16, 2024
@affeldt-aist affeldt-aist force-pushed the fixes_1092 branch 3 times, most recently from 6eb8368 to 555c57c Compare April 16, 2024 11:47
@affeldt-aist
Copy link
Member Author

mulr_rev definition unfolded, as discussed during the last MathComp-Analysis dev meeting.

proux01
proux01 reviewed Apr 17, 2024
View reviewed changes
theories/derive.v Outdated Show resolved Hide resolved
@affeldt-aist
Copy link
Member Author

Ok, it looks like the HB.instance for the R^c case is of no use in MathComp-Analysis...

@proux01
Copy link
Collaborator

proux01 commented Apr 17, 2024

Let's remove it then.
Just to be sure, is the revop structure used then?

@affeldt-aist
Copy link
Member Author

I check and report asap.

proux01
proux01 reviewed Apr 24, 2024
View reviewed changes
classical/mathcomp_extra.v Outdated
Comment on lines 616 to 618
Structure revop X Y Z (f : Y -> X -> Z) := RevOp {
fun_of_revop :> X -> Y -> Z;
_ : forall x, f x =1 fun_of_revop^~ x }.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Out of curiosity, what is this used for?

Copy link
Member Author

Choose a reason for hiding this comment

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

TODO: try to remove it

Copy link
Member Author

@affeldt-aist affeldt-aist Apr 24, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

removed <- wrong advertisement :-/

@proux01 proux01 merged commit 4935fce into math-comp:master Apr 24, 2024
24 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@proux01 proux01 proux01 left review comments

@CohenCyril CohenCyril Awaiting requested review from CohenCyril

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

Successfully merging this pull request may close these issues.

move mulr_rev ?
3 participants
@affeldt-aist @CohenCyril @proux01