In this file the functions and theorems involving cross-product and list are collected together. The function prod_list creates a list of all possible pairs from the two original lists.
** Module lib_list_prod Imports lib_list_length lib_list_bool lib_prod assoc = ... : {A|Type}{B|Type}(A->bool)->B->(list (prod A B))->B list_prod_dom = ... : {A|Type}{B|Type}(list (prod A B))->list A cod = ... : {A|Type}{B|Type}(list (prod A B))->list B zip = ... : {A|Type}{B|Type}(list A)->(list B)->list (prod A B) prod_list = ... : {s|Type}{t|Type}(list s)->(list t)->list (prod s t) length_prod = ... : {s|Type}{t|Type}{l1:list s}{l2:list t} Eq (length (prod_list l1 l2)) (times (length l1) (length l2))