| Some definitions of interest. | |
| gt | Def i > j == j < i |
Thm*  i,j: . (i > j)  Prop | |
| int_seg | Def {i..j } == {k:| i  k < j } |
| Thm* m,n:. {m..n} Type | |
| length | Def ||as|| == Case of as; nil  0 ; a.as' ||as'||+1 (recursive) |
| Thm* A:Type, l:A List. ||l|| | |
| Thm* ||nil|| | |
| nat | Def  == {i:| 0i } |
| Thm* Type | |
| select | Def l[i] == hd(nth_tl(i;l)) |
Thm* A:Type, l:A List, n:. 0n   n < ||l|| l[n] A | |
| sum | Def sum(f(x) | x < k) == primrec(k;0; x,n. n+f(x)) |
Thm* n:, f:(n  ). sum(f(x) | x < n) |
About:
 |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |  |
 |