The Coq mailing list

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

Ok, didn't think about that, thanks for the trick!

Btw, why this restriction?

Best
Chantal



Le 03/07/2017 à 13:41, Frédéric Besson a écrit :
> 
> On Mon, 2017-07-03 at 11:28 +0200, Chantal Keller wrote:
>> 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)).
> 
> It seems you can do the same.
> 
> Module Id' (T:Type) (B1 : ID T).
>  Module CT := Copy T.
>  
>  Module Id'' (B2 : ID CT).
> 
> --
> Frédéric
> 
> 
> 
> 
>>
>> 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