The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi Chantal,

What about having an inner module?

Module Id (T:TYPE) (B:ID T).
  Module CT := Copy T.
  Module IId <: ID CT.
    Parameter id : CT.t -> CT.t.
  End IId.
End Id.


Best,
--
Frédéric


On Sun, 2017-07-02 at 23:37 +0200, Chantal Keller wrote:
> Hi,
> 
> This example is useless, but I would like to do domething similar to:
> 
> 
> Module Type TYPE.
>   Parameter t : Type.
> End TYPE.
> 
> Module Copy (T:TYPE) <: TYPE.
>   Definition t := T.t.
> End Copy.
> 
> Module Type ID (O:TYPE).
>   Parameter id : O.t -> O.t.
> End ID.
> 
> Module Id (T:TYPE) (B:ID T) <: ID (Copy T).
> 
> 
> Coq 8.6 complains about the last statement: "Error: A module cannot
> be
> applied to another module application or with-expression; you must
> give
> a name to the intermediate result module first."
> 
> How can I give a name to the nested application since I want to use
> it
> in the signature?
> 
> Thanks
> Chantal