    Next: Other list functions Up: List Previous: Partial List functions

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

Lego
Fri May 24 19:01:27 BST 1996