mathlib3
2ab31f91 - chore(*): use new `extends_priority` default of 100 (#4066)

Commit
5 years ago
chore(*): use new `extends_priority` default of 100 (#4066) This is the first of (most likely) two PRs which remove the use of `set_option default_priority 100` in favor of per-instance priority attributes, taking advantage of Lean 3.19c's new default priority of 100 on instances produced by `extends`.
Author
Parents
Loading