The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello,

I want to declare such modules:

Module Type Sig.

  Definition T : Type := nat.

  Parameter  f : T -> T.

  Definition g (t : T) : T := f (f t).

End Sig.

Module Impl <: Sig.

  Definition f (t : T) : T := t * 2.

End Impl.

But this is impossible due two reasons:

1. In Impl I don't see definition T from Sig.
   
2. I need to define T and g again in Impl.

First can be solved by putting line "Declare Module Import X : Sig.",
but I am not sure that this line is ok.

Second could be solved by placing definitions T and g into separate module and importing it as argument. But because of mutual definition it becomes difficult:

Module Common.
  Definition T : Type := nat.
  Definition g (t : T) : T := f (f t).
  (* Don't know about f here :( *)
End Common.

Module Type Sig (C : Common).

  Parameter  f : T -> T.

End Sig.

Module Impl (C : Common) <: Sig C.

  Definition f (t : T) : T := t * 2.

End Impl.

So, how to implement that with minimum effort?

Sincerely,
Kirill Taran