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.

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

deal with unwanted side-effects of #3006 #5336

Merged
merged 1 commit into from
Jan 19, 2023

Conversation

ThomasBreuer
Copy link
Contributor

@ThomasBreuer ThomasBreuer commented Jan 19, 2023

- Let the filters created by `DeclareHandlingByNiceBasis` imply
  `IsFreeLeftModule`.
  This was the case before the changes from gap-system#3006, and this change fixes
  the problem described in gap-system#5322, as I had sketched in the discussion of gap-system#5325.
- Document this change (following gap-system#5325).
- Increase the rank of `IsHandledByNiceBasis` by 2.
  Then we get back to the rank before the changes from gap-system#3006.
  This way, the `\in` method with second argument in
  `IsFreeLeftModule and IsHandledByNiceBasis` is again ranked higher than
  the one with second argument `IsFreeLeftModule and IsFiniteDimensional`.
  The bug described in issue gap-system#5334 which has been found because of the
  reordering of these two methods (due to gap-system#3006)
  gets fixed via pull request gap-system#5335,
  now we can return to the better method ordering.
  (I do not like uprankings, but I have no better idea to solve this problem.)
@ThomasBreuer ThomasBreuer added kind: bug Issues describing general bugs, and PRs fixing them topic: library release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes labels Jan 19, 2023
@fingolfin fingolfin enabled auto-merge (rebase) January 19, 2023 23:40
@fingolfin fingolfin merged commit 38f2adb into gap-system:master Jan 19, 2023
@ThomasBreuer ThomasBreuer deleted the TB_nice_basis_filter branch January 20, 2023 08:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Issues describing general bugs, and PRs fixing them release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes topic: library
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants