next up previous contents
Next: The Relation Adjoin Up: List Previous: Other list functions

Lists and products

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
  lib_list_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))