The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

I want to describe some polymorphic operations which depend on typeclasses and organize them in separate files. What is the best way to achieve this?

So, I have a file Monitor.v in which I have the following incantations at the top (Lattice, BoundedLattice, DistributiveLattice are typeclasses defined elsewhere):

```

Variable (Val : Type).
Context {lattice_val : Lattice Val}.
Context {boundedLattice_val : BoundedLattice Val}.
Context {distributiveLattice_val : DistributiveLattice Val}.

```

and below that, there are several things which work properly only if there is a meaningful type Val with all the typeclass constraints.

I want to be able to import the module Monitor.v from inside other files and use the definitions in it. When I do so, I want to instantiate Val and the typeclasses with specific instances. How do I do this? It appears that even though some of the imported things require a specific type be instantiated for Val, there is no way to describe what the relevant instances for the typeclasses are.

My goal here is to be able to extract code for different instantiations of Val and with different typeclasses.

--Agnishom