coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Elie Soubiran" <elie.soubiran AT gmail.com>
- To: "Julien Tesson" <julien.tesson AT univ-orleans.fr>
- Cc: "Mailing list Coq" <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Module derivation ?
- Date: Wed, 17 Sep 2008 10:37:59 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=kRza91/ztXIsE8WMtNx/hQnNv+JRUFRHMqFklj7GCQI7cEqE56WEAYT3Q+KjczG9Rb bd73/I2PF0DopSP8tqDheEttB6nNBsbcT3SI/GbF4BPQlK2DPHbc20sHjBl0bWlSUMUz 4caKoCJhbrVurnwtCcql7zmzAEEz03jQCi+iI=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
You can do :
Module Type A(B_impl : B).
...
End A.
Module Type A2(B_impl : B).
Include Type A B.
The Include feature works with all module / module type expressions.
Elie
2008/9/16 Julien Tesson
<julien.tesson AT univ-orleans.fr>:
>
> Thanks Elie and Stéphane, I have installed the Beta version and it works
> great ...
> but it lead me to a new (but similar) modelling problem :
> I'd like to extend a Higer-order module type but it seems not possible.
> example :
> Module Type A(B_impl : B).
> ...
> End A.
>
> Module Type A2(B_impl : B).
> Include Type A.
> here coqtop respond "You cannot Include a higher-order Module or Module
> Type."
>
> Is there a way to Include A applied to B_impl ?
>
> Julien.
>
>
- [Coq-Club] Module derivation ?, Julien Tesson
- Re: [Coq-Club] Module derivation ?, Stéphane Lescuyer
- Re: [Coq-Club] Module derivation ?,
Elie Soubiran
- Re: [Coq-Club] Module derivation ?,
Julien Tesson
- Re: [Coq-Club] Module derivation ?, Luke Palmer
- Re: [Coq-Club] Module derivation ?, Luke Palmer
- Re: [Coq-Club] Module derivation ?, Elie Soubiran
- Re: [Coq-Club] Module derivation ?,
Julien Tesson
Archive powered by MhonArc 2.6.16.