| Some definitions of interest. |
|
ge | Def ij == ji |
| | Thm* i,j:. (ij) Prop |
|
listp | Def A List == {l:(A List)| (0<||l||) } |
| | Thm* A:Type. A List Type |
|
length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | Thm* A:Type, l:A List. ||l|| |
| | Thm* ||nil|| |
|
map | Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')]
Def (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 |