Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Module derivation ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Module derivation ?


chronological Thread 
  • 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:50:20 -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=GqFdGbXI3B6LqPPZlncfYvin2vEzg/fNGpxW32MoYSSKYqQlY9YyXjfGiZiQ2RkYSV 8EylWguktHXX2z5LnGqhtLyTcGbmgTy2b+Us+InRLvM4bZVaIc0q8N8ZSdGC5iSWRst+ s27IWmyeVjnqjpvrc4Mwqm+8xw5Yg70MjLuPw=
  • 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.
> 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 ?

Module Type A2(B_impl : B).
  Module Type A' := A B_impl.
  Include Type A'.


There might be a shorthand for those two, but the obvious ones that
came to mind didn't work.

Luke



Archive powered by MhonArc 2.6.16.

Top of Page