dot notation with Multiplicative

Stream: mathlib4

[Filippo A. E. Nuccio]

This dot notation for Multiplicative no longer works

import Mathlib.Algebra.Group.TypeTags

example (a : Multiplicative ℤ) : a.toAdd = 0 := by
  sorry
-- invalid field notation, function 'Multiplicative.toAdd' does not have argument with type (Multiplicative ...) that can be used, it must be explicit or implicit with a unique name

and I find myself writing

example (a : Multiplicative ℤ) : Multiplicative.toAdd a = 0 := by
  sorry

Is this expected?

[Yaël Dillies]

This is the general issue with bundled morphisms not taking dot notation anymore. This is really annoying.

[Filippo A. E. Nuccio]

Indeed!

[Eric Rodriguez]

Have we made an RFC for this? Maybe the solution is to upstream something like FunLike, or an annotation on a type that says that 'this type should be coerced to a function to allow dot notation'

[Filippo A. E. Nuccio]

Eric Rodriguez said:

Have we made an RFC for this? Maybe the solution is to upstream something like FunLike, or an annotation on a type that says that 'this type should be coerced to a function to allow dot notation'

RFC?

[Yaël Dillies]

Reasonable Feature Cemetery Request For Comment

[Eric Rodriguez]

The let one is doing pretty well :)