Next: List functions with booleans Up: List Previous: List Definitions

## List Basics

This file defines some basic list functions--where basic really just means pure list functions which do not require any other datatype. These functions include a head function--hd which takes an extra argument which is the value returned for a empty list, tail, fold, append, map and reverse. Some theorems about these functions are also given (but not enough).

``` ** Module lib_list_basics Imports lib_list
singleton = ... : {t|Type}t->list t
hd = ... : {t|Type}t->(list t)->t
tail = ... : {t|Type}(list t)->list t
fold = ... : {s|Type}{t|Type}(t->s->t)->t->(list s)->t
foldright = ... : {B|Type}{A|Type}(A->B->B)->(list A)->B->B
foldleft = ... : {B|Type}{A|Type}(A->B->B)->(list A)->B->B
map = ... : {s|Type}{t|Type}(s->t)->(list s)->list t
append = ... : {t|Type}(list t)->(list t)->list t
tack = ... : {t|Type}t->(list t)->list t
reverse = ... : {t|Type}(list t)->list t
cons_injective = ... :
{t|Type}{k,l|list t}{x,y|t}(Eq (cons x k) (cons y l))->
Eq (tail (cons x k)) (tail (cons y l))
cons_inj = ... :
{s|Type}{a,b|s}{xs,ys|list s}(Eq (cons a xs) (cons b ys))->
and (Eq a b) (Eq xs ys)
l_not_cons_l = ... : {t|Type}{l:list t}{x:t}not (Eq l (cons x l))
append_cons = ... :
{t|Type}{k,l:list t}{x:t}
Ex2 ([y:t][j:list t]Eq (append k (cons x l)) (cons y j))
nil_not_append_cons = ... :
{t|Type}{x:t}{k,l:list t}not (Eq (nil t) (append k (cons x l)))
append_assoc = ... :
{t|Type}{j,k,l:list t}
Eq (append j (append k l)) (append (append j k) l)
append_nil = ... : {t|Type}{l:list t}Eq (append l (nil t)) l
append_reverse = ... :
{t|Type}{l,m:list t}
Eq (reverse (append l m)) (append (reverse m) (reverse l))
append_strict = ... :
{t|Type}{k,l:list t}(Eq (append k l) (nil t))->
and (Eq k (nil t)) (Eq l (nil t))
double_reverse_is_identity = ... :
{t|Type}{l:list t}Eq (reverse (reverse l)) l
foldright_append_lem = ... :
{s|Type}{t|Type}{g:s->t->t}{G,H:list s}{b:t}
Eq (foldright g (append G H) b) (foldright g G (foldright g H b))
foldleft_append_lem = ... :
{s|Type}{t|Type}{g:s->t->t}{G,H:list s}{b:t}
Eq (foldleft g (append G H) b) (foldleft g H (foldleft g G b))```

Lego
Fri May 24 19:01:27 BST 1996