-
-
Notifications
You must be signed in to change notification settings - Fork 719
remove dead code in categories/rings #38884
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
base: develop
Are you sure you want to change the base?
Conversation
|
I am not quite sure this is "dead code". Untested code for sure, ja. |
|
Documentation preview for this PR (built with commit 3119816; changes) is ready! 🎉 |
|
Indeed, you are right. Should we make this a doctest? |
|
Should we (i.e., I) add this as a test to |
4a4f592 to
cf7c8d1
Compare
|
I am not so sure. Maybe we can think about that again once the big changes are merged ? |
Yes, of course! Note that the tests show that the code is not so useful for principal ideal domains without gcd. |
|
#38821 has now been merged I believe. |
|
There are doctest failures. |
The removed line was marked as dead by codecov in #38821. For safety, we remove it in a separate pull request.
Dependencies: #38821