The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

Hi Frédéric,

Thanks for your answer. This works if the nested application is in the
resulting signature of the module, but how to deal with arguments? See e.g.

Module Id' (T:TYPE) (B1:ID T) (B2:ID (Copy T)).

Best
Chantal



Le 03/07/2017 à 10:01, Frédéric Besson a écrit :
> 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