coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Module derivation ?

From: "Luke Palmer" <lrpalmer 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: Tue, 16 Sep 2008 22:53:55 -0600
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=xVGD1sVeLhipDqHh4Q+yUqMKYFPssuhYiz7irY7dSs7B8xvtDYdz/bk4z8znl9nc4g 37PrJmRUVTmqC5UONc2+Ha7hWMZgg21CWIONE/JLwpXYycOpnYtRk4MQrXsf+Xc08hvV AGoi35As37k/rT1qmq7A7jp3hobph40sryszo=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.

Keep in mind that modules are not first-class. As you start needing
to do more complex things, you might consider using Records instead.
The instantiation syntax is a bit uglier (for no good reason AFAICT),
but they are much more flexible.

Luke

[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