Commit 2025-09-25 02:45 6d9efa4a

View on Github →

feat(simps): allow adding arbitrary attributes (#29911)

This deprecates mfld_cfg, attributes now need to be given as a Syntax object, which is not nice to do globally. (Storing attributes as Array Attribute also didn't work, I believe because the attribute needs to be elaborated and applied in the same TermElabM.run snippet.)

Estimated changes

Modified Mathlib/Algebra/Group/Embedding.lean

Modified Mathlib/CategoryTheory/Functor/Basic.lean

Modified Mathlib/CategoryTheory/Functor/Category.lean

modified theorem CategoryTheory.Functor.flip_map_app

Modified Mathlib/CategoryTheory/Iso.lean

Modified Mathlib/CategoryTheory/NatIso.lean

Modified Mathlib/Data/Bundle.lean

Modified Mathlib/Logic/Embedding/Basic.lean

Modified Mathlib/Logic/Embedding/Set.lean

Modified Mathlib/Logic/Equiv/Defs.lean

modified def Equiv.conj

modified def Equiv.sigmaCongrLeft

Modified Mathlib/Logic/Equiv/Option.lean

Modified Mathlib/Logic/Equiv/PartialEquiv.lean

Modified Mathlib/Logic/Equiv/Prod.lean

Modified Mathlib/Tactic/Simps/Basic.lean

deleted def hasSimpAttribute

Modified Mathlib/Topology/PartialHomeomorph.lean

Modified Mathlib/Topology/VectorBundle/Basic.lean

Modified MathlibTest/Simps.lean

added def Grind.foo

added def hasSimpAttribute