The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

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