nil ; a.as' [(f(a)) / map(f;as')] (recursive)
A,B:Type, f:(A
B), l:A List. map(f;l) 
B ListA,B:Type, f:(AB), l:A List
. map(f;l) B List| Who Cites map? | |
| 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: | map(f;as) | has structure: | map(f; as) |
About:
 |  |  |  |  |
 |  |  |  |  |  |