Sum and product types as type class instances

Stream: general

[Eric Wieser]

I've been trying to rewrite finsupp.finsupp_prod_equiv to not require add_comm_monoid x. I've managed to do so, but i instead needed to add a pair of decideable_eq y instances instead.

What's the mathlib way to provide both proofs?
Am I on a road to hell with [inst : add_comm_monoid γ ⊕ (decidable_eq ii × decidable_eq jj)], then using cases inst to pick between two different proofs / definitions?
Is the done thing just to have finsupp_prod_equiv and finsupp_prod_equiv'?

[Scott Morrison]

Yes to both the 2nd and 3rd questions. :-)

[Floris van Doorn]

From the module doc of finsupp:

This file is a `noncomputable theory` and uses classical logic throughout.

So can't you just use classical.prop_decidable for both instance arguments?