## Stream: general

### Topic: Sum and product types as type class instances

#### Eric Wieser (Jul 23 2020 at 18:05):

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 (Jul 23 2020 at 22:53):

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

#### Floris van Doorn (Jul 23 2020 at 23:01):

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?

Last updated: May 08 2021 at 10:12 UTC