mathlib
606be81d - perf(tactic/ext): NEVER USE `user_attribute.get_param` (#2674)

Commit
6 years ago
perf(tactic/ext): NEVER USE `user_attribute.get_param` (#2674) Refactor the extensionality attribute a bit so that it avoids `get_param`, which is a performance nightmare because it uses `eval_expr`. ```lean import all set_option profiler true example (f g : bool → bool → set bool) : f = g := by ext -- before: tactic execution took 2.19s -- after: tactic execution took 33ms ```
Author
Parents
Loading