Commit 2026-02-02 23:54 f66351d7

perf(Tactic/Translate): merge some environment extensions (#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