The Coq mailing list

[bingzhou <bingzhou.zheng AT gmail.com>]

Hi,

I am not familiar with the dependent pattern-matching, and I want to define a
function below 

set-vector-product: 
 (T : Set) -> (n : nat) -> Vector (set T) n -> set (Vector T n)
set-vector-product T [] [] = true
set-vector-product T (s :: ss) (a :: as) = s a /\ set-vector-product T ss as

I wonder if someone can help me define it, or give me some references.

Thanks a lot,
Bingzhou   


Require Import Sets.Ensembles.
Require Import Bool.Bvector.

Section SET.

 Definition set (T : Type) := Ensemble T.

 Fixpoint setVecProd (T : Type) (n : nat) : 
            vector (set T) n -> vector T n -> Prop := ???
End SET.