Length-like list functions

This section contains the list functions which require the natural number datatype; the most important of these functions is the ``length'' function which returns the length of a list. Also given is the nth function which returns the element of a list and a function called build_list which constructs the list corresponding to the first ``n'' elements of a stream represented as a function from nat to the elements of some set.

 ** Module lib_list_length Imports lib_list_basics lib_nat_Lt
  length = ... : {s|Type}(list s)->nat
  nth = ... : nat->{t|Type}(list t)->t->t
  build_list = ... : {s|Type}(nat->s)->nat->list s
  list_length_induction = ... :
    {t|Type}{P:(list t)->Prop}
    ({l:list t}({x:list t}(Lt (length x) (length l))->P x)->P l)->
    {k:list t}P k
  length_zero_nil = ... :
    {s|Type}{l:list s}(Eq (length l) zero)->Eq l (nil s)
  length_map = ... :
    {s|Type}{t|Type}{l:list s}{f:s->t}Eq (length (map f l)) (length l)
  length_build_list = ... :
    {s|Type}{f:nat->s}{n:nat}Eq (length (build_list f n)) n
  length_append = ... :
    {s|Type}{l1,l2:list s}
    Eq (length (append l1 l2)) (plus (length l1) (length l2))