Commit f66351d
committed
perf(Tactic/Translate): merge some environment extensions (leanprover-community#34685)
This PR merges the `translations` and `argInfoAttr` environment extensions used in `to_additive` and `to_dual` into a single environment extension. Arguably, this makes the implementation cleaner, because data that corresponds to eachother is put in the same place together. Moreover, this should lead to a performance improvement because the very existence of persistent environment extensions increases import times.
This PR also changes one implementation detail: when translating a constant based on a prefix of its name, such as in `Foo.casesOn` given a translation of `Foo`, We inherit the `relevant_arg` argument from the main translation. This results in a test case succeeding that previously failed.
See [#mathlib4 > Performance cost of environment extensions](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Performance.20cost.20of.20environment.20extensions/with/571319988)1 parent 7723d00 commit f66351d
4 files changed
Lines changed: 106 additions & 114 deletions
0 commit comments