A,B,C:Type, f:(B
C), g:(AB). f o g 
AC
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 Type| Some definitions of interest. | |
| compose | Def (f o g)(x) == f(g(x)) |
| Thm* A,B,C:Type, f:(BC), g:(AB). f o g AC | |
| 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 | |
| top | Def Top == Void given Void |
| Thm* Top Type |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |  |  |