A,B:Type{i}, f:(A
B), C:Type{i'}, P:((B List)C). P o f 
(A List)C
nil ; a.as' [(f(a)) / map(f;as')] (recursive)A,B:Type, f:(AB), l:A List. map(f;l) B ListA,B:Type, f:(AB), l:A List
. map(f;l) B List| Who Cites compose map? | |
| compose_map | Def P o evt(L) == P(map(evt;L)) |
| Thm* A,B:Type{i}, f:(AB), C:Type{i'}, P:((B List)C). P o f (A List)C | |
| map |
Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')] (recursive) |
|
Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List | |
|
Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List |
| Syntax: | P o evt | has structure: | compose_map(P; evt) |
About:
 |  |  |  |  |
 |  |  |  |  |  |