The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

As far as I understand the Module mechanism, "(Import T : TKV)" does not "import" in the sense you think of.
For me, this parameterize your module by two modules of module type TKV, one being "T" and the other being… "Import".

2014-06-11 6:18 GMT+02:00 Christopher Ernest Sally <christopherernestsally AT gmail.com>:

Hello Beta

Well, I've been trying to write a library and this was part of my attempt at learning how to write interfaces/module types.

I've figured it out now though. It has to do with the incremental style (of the std lib) of building interfaces. The Import statement is there because we want the 'k's  arbitrary as possible (specifically, we don't know they're ordered) and then later on build another interface where they are.

I've include a worked example.

Warm regards
Chris

On 5 June 2014 00:22, Beta Ziliani <beta AT mpi-sws.org> wrote:

On Wed, Jun 4, 2014 at 5:04 AM, Christopher Ernest Sally
<christopherernestsally AT gmail.com> wrote:
> Hi all
>
> I'm trying to learn how to write modules/module types.
>
> I tried out the example at cocorico and am now try to do a
> interface-implementation thing, but am getting the error incompatible module
> type when I try to close the implementation module (called "Implementation"
> in file B.v)
>
> I include the files here. Could any point out what I'm doing wrong? Thanks!

What is exactly what you want to do?  At first sight I (and I guess
Coq) cannot make the connection between the type ht and the product
type.  If you move ht into A and provide ht as  [list (X.t * Y.t)], it
should work.

Best,
Beta

>
> Warm regards
> Chris
>
> (* file A.v *)
> Module Type TKV.
> Parameter ht k v : Type.
> End TKV.
>
>
> Require Import Orders Equalities.
>
> Module Type Interface (K : OrderedType)(V : DecidableType)
> (Import T : TKV).
>
> Parameter empty : ht.
>
> End Interface.
> (* A.v *)
>
>
> (* B.v *)
> Require A. (* of course I have already compiled A *)
> Include A.
> Require Import List Bool Orders Equalities.
>
> Module Implementation (X : OrderedType)(Y : DecidableType)
>
> <: A.Interface X Y.
>
> Definition empty := @nil (prod X.t Y.t) .
>
> End Implementation.
> (* B.v *)

--
.../Sedrikov\...