next up previous contents
Next: Lists and products Up: List Previous: Length-like list functions

Other list functions

This section (so far) contains the boolean-valued function which tests to see of two lists have the same length. This function requires both the boolean and the natural number datatypes and is separated to reduce the dependencies.

 ** Module lib_list_misc Imports lib_list_length lib_list_partial
  same_length = ... : {s|Type}{t|Type}(list s)->(list t)->bool
  Eq_length_imp_same_length_true = ... :
    {t|Type}{l,m:list t}(Eq (length l) (length m))->
    is_true (same_length l m)