The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

×óÓ£ wrote:
> I'm trying to define a function to compute the combination of sets, 
> which pick an element from every set and combine into another set. Let 
> ci be the number of element in set i .The total number of elements in 
> result set will be

Since you're talking about numbers, I presume you only mean to deal with 
_finite_ sets? If so, you have some representation choices to make. 
Certainly the function is easy to implement over lists, though you might 
want to ensure lack of duplicates in lists, for a fully faithful 
representation. The "list combination" function is a standard exercise 
in functional programming, bringing in very little that is new to Coq 
compared to OCaml.