The Coq mailing list

[Jaap Boender <jaapb AT kerguelen.org>]

Hello all,

I'm trying to implement a calculus in Coq, which involves the following 
inductive type (minimalised a bit, but this is the idea):

Parameter Atom: Type.
Parameter Group: Type
Inductive thing (S: Group): Type :=
  nd_atom: Atom -> thing S
| nd_impl: thing S -> thing S -> thing S
| nd_and: thing S -> thing S -> thing S
| nd_or: thing S -> thing S -> thing S.

I'd now like to create sets of 'thing'  using FSets, so I've put thing in a 
module, which contains things like

Module ThingMod.
  Definition t := Resource.
  Function eq {S: Group} (x y: Resource S): Prop :=
   (...)
End ThingMod.

and now I'm trying to define a WSet based on this module, but I'm running 
into 
a problem: my ThingMod.t is not  a Type, but a Group -> Type. That's not 
surprising, but what I've been wrestling with: is there a way to lift this 
Group parameter to the module level? I'd like to be able to define sets that 
are parametrised by S, such that the elements of these sets are all of type 
'thing S' - but I haven't been able to find how. Am I overlooking something 
really basic, or is this just not possible? Or should I do this differently? 
Any help would be appreciated.

thanks,

  Jaap