The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

It would depend on the context.  If it's the n-fold Cartesian product
of a set A, then you'd probably want to use Vector.t A n.  If it's a
statement of the form "let A_1, ..., A_n be sets; then something
happens on A_1 x A_2 x ... x A_n" then you probably want to encode the
sequence as an element of list Type, and define either

Fixpoint list_prod (l : list Type) : Type :=
match l with
| nil => unit
| cons A l' => (A * list_prod l')%type
end.

or

Inductive list_prod : list Type -> Type :=
| list_prod_unit : list_prod nil
| list_prod_pair : forall (A:Type) (l:list Type), A -> list_prod l ->
list_prod (cons A l).

The first one would probably be easier to work with, at least at first.
-- 
Daniel Schepler

On Thu, Aug 28, 2014 at 6:54 PM, coqcdp 
<coqcdpnxj AT 163.com>
 wrote:
> Dear everyone,
>                           I want to formalize an algebra text book these
> days ,but I have a problem when I try  to define "Catesian product".Could
> you tell
>               me how to define Cartesian product of n (n can be any nat)
> sets?   Thanks.
>          Yours Sincerely,
>                                     D.P.Chen.
>
>