module R R

Stream: mathlib4

[Johan Commelin]

Do we have a standard fix for

failed to synthesize instance
  @Module R R (@Ring.toSemiring R (@CommRing.toRing R inst✝))
    (@AddCommGroup.toAddCommMonoid R (@Ring.toAddCommGroup R (@CommRing.toRing R inst✝)))

[Eric Wieser]

If so, we should record it at lean4#2074

[Eric Wieser]

I suggested there that we make it possible to locally enable/ disable TC eta, as I think that would help unblock the port until we have a better solution

[Kevin Buzzard]

lean4#2074