| Some definitions of interest. |
|
map | Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')]
Def (recursive) |
|
| Thm* A,B:Type, f:(A B), l:A List. map(f;l) B List |
|
| Thm* A,B:Type, f:(A B), l:A List . map(f;l) B List |
|
pi1 | Def 1of(t) == t.1 |
|
| Thm* A:Type, B:(A Type), p:(a:A B(a)). 1of(p) A |
|
pi2 | Def 2of(t) == t.2 |
|
| Thm* A:Type, B:(A Type), p:(a:A B(a)). 2of(p) B(1of(p)) |
|
zip | Def zip(as;bs)
Def == Case of as
Def == Canil nil
Def == Caa.as' Case of bs; nil nil ; b.bs' [<a,b> / zip(as';bs')]
Def (recursive) |
|
| Thm* T1,T2:Type, as:T1 List, bs:T2 List. zip(as;bs) (T1 T2) List |