The Coq mailing list

[Scott Lawrence <srl AT umd.edu>]

Hi all,

Many of the same things can be done via `Module Type` and `Module` as with 
`Class` and `Instance`. Are there any good rules of thumb for when to use 
which? For example, either could be used to define VectorSpace < 
NormedVectorSpace < BanachSpace -- is there a reason to pick one over the 
other?

(Somewhat pettily, I find the syntax resulting from using the module system to 
be far cleaner. I also note that the documentation declares type classes to 
be very experimental.)

Thanks,

--
Scott Lawrence