nil ; a.as' f(a).map(f;as') (recursive)
A,B:Type, f:(A
B), 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 |
| Syntax: | map(f;as) | has structure: | map(f; as) |
About:
 |  |  |  |  |
 |  |  |  |  |  |