| Who Cites compose list? |
|
compose_list | Def compose_list(L) == reduce( p,q. p o q; x.x;L) |
| | Thm* T:Type, L:(T T) List. compose_list(L) T T |
|
compose | Def (f o g)(x) == f(g(x)) |
| | Thm* A,B,C:Type, f:(B C), g:(A B). f o g A C |
|
reduce | Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) (recursive) |
| | Thm* A,B:Type, f:(A B B), k:B, as:A List. reduce(f;k;as) B |