Field names collision for type class inheritance

Stream: mathlib4

[Qi Ge]

Suppose I want to

class Foo (A: Type*) extends Class1 A, Class2 A where
  -- ...

but both Class1.bar and Class2.bar are defined for different type, what should I do?

[Qi Ge]

This arises in practice for LinearMap and MulActionHom where both define map_smul' field for compatibility with respect to different actions.

[Adam Topaz]

in lean3 it was possible to write ... extends Class1 A, Class2 A renaming foo -> bar ... but I don't think this has been introduced in Lean4.

[Qi Ge]

MulActionHom is relatively simple I will try hardcoding it and see how far I can go for now...

[Eric Rodriguez]

Does it matter in lean4? I thought extends is just sugar for generating projections

[Eric Wieser]

It also affects dot notation

[Eric Wieser]

But I guess for class that's irrelevant anyway