mathlib
77c5dfe2 - perf(*): avoid `user_attribute.get_param` (#3073)

Commit
5 years ago
perf(*): avoid `user_attribute.get_param` (#3073) Recent studies have shown that `monoid_localization.lean` is the slowest file in mathlib. One hundred and three seconds (93%) of its class-leading runtime are spent in constructing the attribute cache for `_to_additive`. This is due to the use of the `user_attribute.get_param` function inside `get_cache`. See the [library note on user attribute parameters](https://leanprover-community.github.io/mathlib_docs/notes.html#user%20attribute%20parameters) for more information on this anti-pattern. This PR removes two uses of `user_attribute.get_param`, one in `to_additive` and the other in `ancestor`.
Author
Parents
Loading