mathlib3
3965e063 - chore(*): use new `extends_priority` default of 100, part 2 (#4101)

Commit

5 years ago

chore(*): use new `extends_priority` default of 100, part 2 (#4101) This completes the changes started in #4066.

References

Author

rwbarton

Parents