..., and make clear (again: in a different Impl module?) when a module implements such a spec.
@gallais 's #2975 reminds me that the mess that is Data.Nat.DivMod and its friend Data.Nat.DivMod.WithK might be a lot (only a bit?) cleaner if each such module is shown as implementing a (much simpler) Data.Nat.DivModSpec. Esp. if that allows us to also functorise such specifications (in the SML sense) so that Data.Nat.DivModSpec depends on the specification of the type Fin implementing the remainder field... etc.
cf. recent discussions of AVL trees #2961 #2970 #2969 and prior Zulip discussion
..., and make clear (again: in a different
Implmodule?) when a module implements such a spec.@gallais 's #2975 reminds me that the mess that is
Data.Nat.DivModand its friendData.Nat.DivMod.WithKmight be a lot (only a bit?) cleaner if each such module is shown as implementing a (much simpler)Data.Nat.DivModSpec. Esp. if that allows us to alsofunctorise such specifications (in the SML sense) so thatData.Nat.DivModSpecdepends on the specification of the typeFinimplementing theremainderfield... etc.cf. recent discussions of AVL trees #2961 #2970 #2969 and prior Zulip discussion