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
[Merged by Bors] - chore: reduce imports of Data.List.Defs #8635
Conversation
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
* was inferring `Nat` as arguments for `R` * note that `[Monoid M]`/`[Monoid N]` are variables
Pushed a couple small fixes (test imports + type signature—a win for the unused variables linter!); if it builds, then LGTM :) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
|
||
-/ | ||
|
||
set_option autoImplicit true |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you just remove this line and add the missing type declaration for alpha below?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sure. It still makes me sad. :-)
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Currently `Data.List.Defs` depends on `Algebra.Group.Defs`, rather unnecessarily. (This then prevents importing `Data.List.Defs` into `Tactic.Common`, without breaking various `assert_not_exists` statements.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Currently `Data.List.Defs` depends on `Algebra.Group.Defs`, rather unnecessarily. (This then prevents importing `Data.List.Defs` into `Tactic.Common`, without breaking various `assert_not_exists` statements.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
Currently
Data.List.Defs
depends onAlgebra.Group.Defs
, rather unnecessarily.(This then prevents importing
Data.List.Defs
intoTactic.Common
, without breaking variousassert_not_exists
statements.)