The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hi everybody,
I want to formalise finite multi-sets using the module system of Coq
Unfortunately I found some problems that I was unable to solve
Let's take the simplified following example

Inductive Form(A:Set):Set:=
|atom:A->Form A
|impl: Form A ->Form A ->Form A.

Module Type Ord.
Parameter t:Set.
(* .... *)
End Ord.

Module Type Multi_Set.
Declare Module O:Ord.
Definition t:=O.t.
Parameter m:Set.
(* ... *)
End Multi_Set.

Module Type At.
Parameter A:Set.
End At.

(* functor *)
Module setOrd(AT:At)<:Ord.
Definition t:=Form AT.A.
End setOrd.

(* in this module I want to manipule multi-sets containing
 formulaes built from a specific set of atoms AT.A)
Module use_multi(AT:At)(ms:Multi_Set with Module O:= (setOrd AT)).

Coq system generates a syntax error for this last declaration...
Can anyone tell me why ??

Otherwise, if such declaration is not possible (because of the use of 
the functor
setOrd ), how can I express the functor use_multi??
Thanks a lot in advance
Houda

--
==============================
| /\    Houda ANOUN     /\   |
|  -       LaBRI        -    |
| 351 Cours de la libération |
|      33405 Talence         |
|phone  : 0540002489         |
|e-mail : 
anoun AT labri.fr
     |
|web    : www.labri.fr/~anoun|
==============================