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