The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

All,

I asked this a while ago, but got no answer, so I am seeing if maybe I can 
try again.

The question: how can I write a “with” clause in a module type that refers to 
a name already defined in the existing module type? That is, I want to write 
something like

Module Type mt’ := mt with Definition foo := fun (x:T) => x.

where mt has the following definition:

Module Type mt.
  Parameter T : Set.
  Parameter foo : T -> T.
End mt.

Or maybe there is some alternative way to update a name in a module type, to 
give it a definition? Any suggestions?

Thanks very much,
-Eddy