| Infinite product would be dependent type, wouldn't it? HOL doesn't come | with dependent types out of the box, and I haven't seen an add-on | library for it.
Indeed, it's not easy to outfit HOL with dependent types. But you can at least have infinite product types that are not dependent, i.e. are parametrized by a type not a term. For example, you can regard the function space A->B as an A-ary product of B's; indeed set theorists often write B^A instead of A->B. Using a variant of this idea, I showed in a TPHOLs 2005 paper how to fake n-ary Cartesian product types so you almost get a kind of dependent type. I interpreted the original question as being about sums and products of numbers, not of types, though maybe I'm completely wrong. In that case I don't know the best HOL4 answer, which is why I didn't reply earlier. But I can give a HOL Light answer if desired. John. ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
