The Coq mailing list

["Eddy Westbrook" <westbrook AT kestrel.edu>]

Hi,

I am having trouble using "with Definition" clauses in module types to give
definitions to fields whose types depend on earlier elements of the module
type. For example, I want to start with the following module type:

Module Type S1.

  Parameter T : Type.
  Parameter f : T -> T.

End S1.


Then I want to create a derived module type S2, where f is defined as the
identity function over T but T still does not have a definition; i.e.,
something like this:

Module Type S2 := S1 with Definition f := fun t => t.

If I write it like the above, Coq tells me it cannot infer the type of the
variable t. But I can't figure out how to refer to the type T of t! Neither of
the following work:

Module Type S2 := S1 with Definition f := fun (t:T) => t.
Module Type S2 := S1 with Definition f := fun (t:S1.T) => t.

Is there any way to get this to work without having to completely redefine S1?

Thanks,
-Eddy