stdpp.base.decide := Coq.Classes.DecidableClass.decide?
stdpp.base.decide
duplicates the functionality of Coq.Classes.DecidableClass.decide
. It is not clear that stdpp.base.decide
provides something better. If so, would it be better to just reuse the functionality Coq.Classes.DecidableClass
?