Library Coq.Logic.DecidableTypeEx
Examples of Decidable Type structures.
A particular case of DecidableType where
the equality is the usual one of Coq.
a UsualDecidableType is in particular an DecidableType.
an shortcut for easily building a UsualDecidableType
An OrderedType can now directly be seen as a DecidableType
(Usual) Decidable Type for nat, positive, N, Z
From two decidable types, we can build a new DecidableType
over their cartesian product.
Similarly for pairs of UsualDecidableType