The Coq mailing list

["Joseph N. Ruskiewicz" <joseph.ruskiewicz AT inf.ethz.ch>]

Hello Coq Club:
   I have been working with modules and have noticed that to declare a 
new Module with parameters, they must be of type of Module.

   Is it not possible to declare a type of say, nat, for a parameter?

   I have played with:

   Module N.
   Parameter x:nat.
   End.

But, that is just declaring x to be an Axiom of the Module.

I would like to be able to use the Module and give it parameters of 
basic types (Z,R,Bool).

Any wisdom?

Thank you again,

Joseph