Re: [Hol-info] HOL-4 Question

[John H. <Joh...@cl...>]

| 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.