The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

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!

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 *)

Attachment: A.v
Description: Binary data

Attachment: B.v
Description: Binary data