The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

Hi,

I think something like:

Module B : A with Definition T := nat.

will work.  I don't remember the precise syntax, but this basically 
specializes the module type for the case where T is nat.  This will expose 
the definition of T without exposing the rest.

-Andrew


On Thu, 3 May 2007, Guillaume Melquiond wrote:

> Hi,
>
> I am trying to use the module system with Coq 8.1 and I don't seem to
> get a sensible behavior. The following example defines an interface A (a
> module type) and an implementation B (a module) for this interface. The
> function g is an implementation detail (not in A, only in B) and it
> should be hidden to the user of module B. So I am typing the following
> script:
>
>        Module Type A.
>          Parameter T : Type.
>          Parameter f : T -> T.
>        End A.
>
>        Module B : A.
>          Definition T := nat.
>          Definition g := S.
>          Definition f := fun x : T => x.
>        End B.
>
>        Import B.
>        Print T.
>        Check (f 0).
>
> Unfortunately, B can not be used at all, as Coq considers the type
> definition T to be opaque. For the last two lines, Coq prints:
>
>        *** [ T : Type ]
>        Error: The term "0" has type "nat" while it is expected to have type 
> "T"
>
> The only way I have found so that I can use B is to replace the type
> specification "B : A" with "B <: A". Coq now prints:
>
>        T = nat
>             : Set
>        f 0
>             : nat
>
> Unfortunately, the implementation detail g now pollutes the global
> scope. The documentation does not describe other ways of defining a
> module of a given type. How can I get a usable module (T not opaque)
> without leaking any implementations details (e.g. hundreds of
> intermediate lemmas)?
>
> Best regards,
>
> Guillaume
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club