The Coq mailing list

[Paolo Herms <paolo.herms AT lri.fr>]

Hi,
more generally you can also use heterogeneous lists as in [1] in which each 
element may have a different type. The type hlist E of heterogeneous lists 
then 
depends on the list of types E of their elements.
In your case you could have a list [a1;a2;b1;a3;b2] of type hlist [A;A;B;A;B]

[1] http://adam.chlipala.net/cpdt/html/DataStruct.html#lab57
-- 
Paolo Herms, PhD
Paris, France


On Sunday 10 March 2013 06:15:16 
mcano.programas AT gmail.com
 wrote:
> Good Night,
> 
> I'm pretty new to coq and all the logic beneath it, but i was wondering if
> it is possible to define a collection of things with different types, the
> thing if i have two inductive definitions and i need a list that can
> contain types of the two definitions, is this possible, maybe can anyone
> give me an example on how to do it?
> 
> Thank you all beforehand.