RingTheory.Finiteness !4#2811

Stream: mathlib4

[Ruben Van de Velde]

I was poking my nose into this, and getting failed to synthesize instance SemilinearMapClass (M →ₗ[R] N) ?m.494659 ?m.494651 ?m.494652 issues - is that something people recognize?

[Eric Wieser]

etaExperiment true?

[Ruben Van de Velde]

Oh, is that what that fixes? Thanks

[Eric Wieser]

If you have any module-related typeclass issue it's likely related to that

[Eric Wieser]

I don't think that's the preferred workaround to lean4#2074, but it's enough to identify it as the cause

[Jireh Loreaux]

I think we're not merging PRs with etaExperiment true in them, so it definitely needs another workaround.

[Eric Wieser]

We definitely have been, although I'm not sure if we intended to

[Matthew Ballard]

Some of the commit messages reference it

[Eric Wieser]

It's also in the source code.