Data.Finset.Pointwise !4#1911

Stream: mathlib4

[Johan Commelin]

There are some issues with typeclass resolution and dangerous instances. My guess is that this is due to the change in direction in which Lean 4 works compared to Lean 3. Should we investigate further?

[Anne Baanen]

I saw one typeclass issue in the commits, in 4afe43d, are there others?

With regards to that commit, Lean 4 being more sensitive to outParams is definitely a known issue. Especially since there are plans to change outParam handling further (lean4#1901) I think it's not worth the effort to do a lot with this on the mathlib side.

[Johan Commelin]

ok, thanks for looking into this