Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
  • To: Andreas K�gi <acepublic AT fastmail.fm>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Newbie Questions on Module Type usage
  • Date: Tue, 16 Sep 2008 08:05:24 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

When you write the following line:

Module M1 : MT1.

You promise that you are going to build a module that satisfies
the interface declared in the module type MT1, so you have to
produce a value named A of type Set, you have to produce an
inductive type of name t and type Set with a constructor T,
and you have to produce a submodule type with the same characteristics
as in the module type MT1 (not an instance of the module MT1sub, but
another module type, with the same name and fields).  The following
session works (in coq-8.2beta4):

Module Type MT1.
 Parameter A: Set.

 Inductive t : Set := T.

 Module Type MT1sub.
   Parameter B: Set.
 End MT1sub.
End MT1.

Module M1 : MT1.

 Definition A := nat.

 Inductive t : Set := T.

 Module Type MT1sub.
   Parameter B: Set.
 End MT1sub.
End M1.

Right now, I don't see why you would want to have a module type
inside another module type (like you did with MT1sub), but it is
possible.

I hope this helps,

Yves






Archive powered by MhonArc 2.6.16.

Top of Page