The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon 
anoun AT labri.fr:

Hi Houda,

 Perhaps the problem comes from taking a module to represent
each multiset. I think that the module system is OK for representing
various implementations of some algebraic structure, but not various
members of the same set of such structures.

 In the latter case, you can use records for representing the multisets
you want to compute the union, inersection ... of which.

Pierre



> Hi everybody,
> Let's define a simpl module type to describe finite multisets:
>  Module Type MSet.
> Parameter A:Set.  (* types  of elements *)
> Paramater X:Set.
> ....
> Parameter empty:X.
> Parameter union :X->X->X.
>
> ....
> (* here we define some notations *)
> Notation "m1 'U' m2":=(union m1 m2) (at level 10):set_scope.
> End MSet.
>
> Suppose that we need to define a functor that takes two multisets as
> parameters
> Module mset_funct (M1 M2:MSet).
>
>
> ....
> End mset_funct.
>
> Inside mset_funct, we are unable to use the notation defined within MSet at
> least for both m1 and m2.
> We can use partially the notation for m1 if we export this module
> Export m1.
> but the problem remains for m2.
>
> Is there a way to solve that problem?
>
> Particularly with PCoq, can we define a new rule for pretty printer that
> replaces 'X.union *x1 *x2' by *x1 U *x2 and so for all modules X?
>
> Thanks a lot in advance
> Houda
>
>
>
> ----------------------------------------------------------------
> This message was sent using IMP, the Internet Messaging Program.
> --------------------------------------------------------
> 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
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.