coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Newbie Questions on Module Type usage

From: Andreas Kägi <acepublic AT fastmail.fm>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Re: Newbie Questions on Module Type usage
Date: Tue, 16 Sep 2008 07:26:22 +0000 (UTC)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Thanks four your help, Yves.
I was probably too much thinking in a Java analogy of interfaces and classes.
I thought I only had to produce a value A of type Set and a module M1sub
satisfying the signature of MT1. But apparently, I cannot use the
definitions/module types defined in a module type within the corresp. module
implementation?

[Coq-Club] Newbie Questions on Module Type usage, Andreas Kägi
- Re: [Coq-Club] Newbie Questions on Module Type usage, Yves Bertot
- [Coq-Club] Re: Newbie Questions on Module Type usage, Andreas Kägi
  - Re: [Coq-Club] Re: Newbie Questions on Module Type usage, Yves Bertot