Commit 2025-05-30 10:05 3bf06aea

feat: when simps is used on inst names, omit the name (#25125) When @[simps] is used on

namespace Foo
@[simps]
instance : Group Foo := ...
end Foo

this now generates the names Foo.mul_def, Foo.inv_def, etc. If Foo has simps projections, these will be used as Foo.mul_proj, Foo.inv_proj (respecting prefixes as usual). This introduces @[simps (nameStem := "")] to opt into the behavior explicitly, and @[simps (nameStem := "instGroup")] to opt out. Note that this does not deprecate the old auto-generated names, as in practice it is tricky to exhaustively list them all, and adding support to simps to generate them does not seem worth the effort. It's perhaps worth noting that we didn't need this feature as much in Lean 3, as there the instances were called instance mul : mul X instead of instance instMul : Mul X, and so we got theorem mul_mul instead of theorem instMul_mul.