coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Jianzhou Zhao" <jianzhou AT seas.upenn.edu>
- To: <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] How to implement a 'module type' in multi files
- Date: Wed, 20 Aug 2008 14:00:05 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
|
I defined a module type as the signature, and now I
am implementing
this signature into a concret module. If the module
type includes
a lot of axioms and parameters to implement, is
there a way to
implement it in more than one file, so that each
file could be smaller.
-jz
|
- [Coq-Club] How to implement a 'module type' in multi files, Jianzhou Zhao
Archive powered by MhonArc 2.6.16.