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
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
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